trying to fix smt instability

Author: mbbarbosa

theories/algebra/ZModPCentered.ec

@@ -80,7 +80,16 @@ qed.
 
 lemma to_crepr_id x :
   (p + 1) %/ 2 - p <= x < (p + 1) %/ 2 => to_crepr x = x.
-proof. smt(). qed.
+proof.
+move=> [Hl Hu]; rewrite /to_crepr /=.
+have Hp := ge2_p.
+case (0 <= x) => Hx.
+- have -> : x %% p = x by apply modz_small; smt().
+  by rewrite ifF /#.
+- have Hxp : (x + p) %% p = x + p by apply modz_small; smt().
+  have -> : x %% p = x + p by rewrite -(modzDr x) Hxp.
+  by rewrite ifT 1:/# /#.
+qed.
 
 lemma to_crepr_eq x y : to_crepr x = to_crepr y <=> zmodcgr x y.
 proof. rewrite /to_crepr /= /#. qed.