prove admit about F.to_nat x mod m

3 files changed, 15 insertions, 6 deletions

diff --git a/src/EdDSARepChange.v b/src/EdDSARepChange.v
index 7a91e4a95..d63e6d14e 100644
--- a/src/EdDSARepChange.v
+++ b/src/EdDSARepChange.v
@@ -11,11 +11,6 @@ Import NPeano.
 
 Import Notations.
 
-Module F.
-  Lemma to_nat_mod {m} (x:F m) : F.to_nat x mod (Z.to_nat m) = F.to_nat x.
-  Admitted.
-End F.
-
 Section EdDSA.
   Context `{prm:EdDSA}.
   Local Infix "==" := Eeq. Local Infix "+" := Eadd. Local Infix "*" := EscalarMult.
@@ -136,7 +131,7 @@ Section EdDSA.
       etransitivity. Focus 2. {
         eapply Proper_option_rect_nd_changebody; [intro|reflexivity].
         eapply Proper_option_rect_nd_changebody; [intro|reflexivity].
-        rewrite <-F.to_nat_mod.
+        rewrite <-F.to_nat_mod by omega.
         repeat (
             rewrite ERepEnc_correct
             || rewrite homomorphism
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index f1a2d15a4..44b422767 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -174,6 +174,13 @@ Module F.
       rewrite <-F.of_Z_mod; reflexivity.
     Qed.
 
+    Lemma to_nat_mod (x:F m) (Hm:(0 < m)%Z) : F.to_nat x mod (Z.to_nat m) = F.to_nat x.
+      unfold F.to_nat.
+      rewrite <-F.mod_to_Z at 2.
+      apply Z.mod_to_nat; [assumption|].
+      apply F.to_Z_range; assumption.
+    Qed.
+
     Lemma of_nat_add x y :
       F.of_nat m (x + y) = (F.of_nat m x + F.of_nat m y)%F.
     Proof. unfold F.of_nat; rewrite Nat2Z.inj_add, F.of_Z_add; reflexivity. Qed.
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 086cc72d4..8257c429f 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -479,6 +479,13 @@ Module Z.
     reflexivity.
   Qed.
 
+  Lemma mod_to_nat x m (Hm:(0 < m)%Z) (Hx:(0 <= x)%Z) : (Z.to_nat x mod Z.to_nat m = Z.to_nat (x mod m))%nat.
+    pose proof Zdiv.mod_Zmod (Z.to_nat x) (Z.to_nat m) as H;
+      rewrite !Z2Nat.id in H by omega.
+    rewrite <-H by (change 0%nat with (Z.to_nat 0); rewrite Z2Nat.inj_iff; omega).
+    rewrite !Nat2Z.id; reflexivity.
+  Qed.
+
   Ltac divide_exists_mul := let k := fresh "k" in
   match goal with
   | [ H : (?a | ?b) |- _ ] => apply Z.mod_divide in H; try apply Zmod_divides in H; destruct H as [k H]