From 5ae4142f0c537ab705c9f00ec023b6885f6ebce9 Mon Sep 17 00:00:00 2001
From: Manuel Barbosa <mbb@fc.up.pt>
Date: Fri, 17 May 2024 18:14:49 +0200
Subject: [PATCH] Removed spurious smt.

---
 proof/correctness/Montgomery.ec | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/proof/correctness/Montgomery.ec b/proof/correctness/Montgomery.ec
index 12c34423..63dee710 100644
--- 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.