Removed spurious smt.

formosa-crypto · May 17, 2024 · 5ae4142 · 5ae4142
1 parent 071b898
commit 5ae4142
Showing 1 changed file with 1 addition and 3 deletions.
diff --git a/proof/correctness/Montgomery.ec b/proof/correctness/Montgomery.ec
@@ -124,9 +124,7 @@ case: (0 <= x) => [le0x|/ltrNge ltx0].
   rewrite modz_small // le0x /= gtr0_norm; [by apply/(ler_lt_trans _ _ _ _ lt1y)|].
   apply/(ltr_le_trans _ _ _ ltx_)/leq_div => //.
   by apply/ltzW/(ler_lt_trans _ _ _ _ lt1y).
-have ->/=: (y %/ 2 <= x %% y).
-+ smt.
-smt.
+by smt(). 
 qed.
 
 lemma smod_div x : smod (x * R) (R ^ 2) %/ R = smod x  R.