diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-10-27 16:03:20 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-10-27 16:03:29 -0400 |
commit | abd5931c3166ccef09e1305f5adc1a82cad0dcd5 (patch) | |
tree | f60c3d1bfc7908ed6ad31613f1c2da5580d8b4ac /src/Util | |
parent | 426f04e98c497feaed59b6604cc78ec5888077fc (diff) |
prove admit about F.to_nat x mod m
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/ZUtil.v | 7 |
1 files changed, 7 insertions, 0 deletions
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] |