diff --git a/src/Arithmetic/MontgomeryReduction/Proofs.v b/src/Arithmetic/MontgomeryReduction/Proofs.v
index e0d8dae5a5..7b6ae5129c 100644
--- a/src/Arithmetic/MontgomeryReduction/Proofs.v
+++ b/src/Arithmetic/MontgomeryReduction/Proofs.v
@@ -127,7 +127,7 @@ Section montgomery.
         break_match; rewrite partial_reduce_correct; t_fin_correct.
       Qed.
 
-      Let m_small : 0 <= m < R. Proof using N'_in_range. auto with zarith. Qed.
+      Let m_small : 0 <= m < R. Proof. auto with zarith. Qed.
 
       Section generic.
         Lemma prereduce_in_range_gen B