diff --git a/src/Arithmetic/BarrettReduction.v b/src/Arithmetic/BarrettReduction.v
index 8be6b0b30c..a037bccb55 100644
--- a/src/Arithmetic/BarrettReduction.v
+++ b/src/Arithmetic/BarrettReduction.v
@@ -118,8 +118,7 @@ Module Fancy.
     Local Notation w := (uweight width). Local Notation eval := (Positional.eval w).
     Context (mut Mt : list Z) (mut_correct : mut = Partition.partition w (sz+1) mu) (Mt_correct : Mt = Partition.partition w sz M).
     Context (mu_eq : mu = 2 ^ (2 * k) / M) (muHigh_one : mu / w sz = 1) (M_range : 2^(k-1) < M < 2^k).
-
-    Local Lemma wprops : @weight_properties w. Proof. apply uwprops; auto with lia. Qed.
+    Local Lemma wprops : @weight_properties w. Proof using width_ok. clear - width_ok. apply uwprops ; lia. Qed.
     Local Hint Resolve wprops : core.
     Hint Rewrite mut_correct Mt_correct : pull_partition.
 
diff --git a/src/Arithmetic/WordByWordMontgomery.v b/src/Arithmetic/WordByWordMontgomery.v
index d75cdc3dde..b0e4caa9b2 100644
--- a/src/Arithmetic/WordByWordMontgomery.v
+++ b/src/Arithmetic/WordByWordMontgomery.v
@@ -650,6 +650,7 @@ Module WordByWordMontgomery.
         Lemma fst_redc_body_mod_N
           : (eval (fst (redc_body A_S))) mod (eval N) = ((eval (fst A_S) - a)*ri) mod (eval N).
         Proof using small_S small_A ri_correct lgr_big S_bound.
+          clear R_numlimbs_nz.
           rewrite fst_redc_body.
           etransitivity; [ eapply Z.div_to_inv_modulo; try eassumption; lia | ].
           unfold a, A_a, A.