Fix a missing mod resolution

Apparently this only triggered in 8.4

1 files changed, 5 insertions, 0 deletions

diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v
index d03bafbb1..e5b74085e 100644
--- a/src/Experiments/DerivationsOptionRectLetInEncoding.v
+++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v
@@ -335,10 +335,15 @@ Lemma FieldToN_correct {m} (x:F m) : FieldToN (m:=m) x = Z.to_N (FieldToZ x). re
 
 Definition natToField {m} x : F m := ZToField (Z.of_nat x).
 Definition FieldToNat {m} (x:F m) : nat := Z.to_nat (FieldToZ x).
+
+Section with_unqualified_modulo2.
+Import NPeano Nat.
+Local Infix "mod" := modulo : nat_scope.
 Lemma FieldToNat_natToField {m} : m <> 0 -> forall x, x mod m = FieldToNat (natToField (m:=Z.of_nat m) x).
   unfold natToField, FieldToNat; intros.
   rewrite (FieldToZ_ZToField), <-mod_Zmod, Nat2Z.id; trivial.
 Qed.
+End with_unqualified_modulo2.
 
 Lemma F_eqb_iff {q} : forall x y : F q, F_eqb x y = true <-> x = y.
 Proof.