trying to fix smt instability

Author: mbbarbosa

theories/algebra/ZModPCentered.ec

@@ -71,7 +71,12 @@ lemma rg_to_crepr x :
 proof. smt(ge2_p rg_asint). qed.
 
 lemma to_crepr_zmodcgr x : zmodcgr x (to_crepr x).
-proof. smt(ge2_p). qed.
+proof.
+rewrite /to_crepr /=; case ((p + 1) %/ 2 <= x %% p) => _.
+- have -> : x %% p - p = x %% p + (-1) * p by ring.
+  by rewrite /zmodcgr modzMDr modz_mod.
+- by rewrite /zmodcgr modz_mod.
+qed.
 
 lemma to_crepr_id x :
   (p + 1) %/ 2 - p <= x < (p + 1) %/ 2 => to_crepr x = x.