trying to fix smt instability

Author: mbbarbosa

theories/algebra/ZModPCentered.ec

@@ -37,8 +37,13 @@ lemma zmodcgr_ceq a b :
      (p + 1) %/ 2 - p <= a < (p + 1) %/ 2
   => (p + 1) %/ 2 - p <= b < (p + 1) %/ 2
   => zmodcgr a b
-  => a = b
-  by case (0 <= a); case (0 <= b); smt().
+  => a = b.
+proof.
+move=> Ha Hb Hcgr.
+have Hp := ge2_p.
+have Hdvd : p %| (a - b) by smt(zmodcgrP).
+smt().
+qed.
 
 lemma zmodcgr_transitive b a c :
   zmodcgr a b => zmodcgr b c => zmodcgr a c.