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/ModularArithmetic/ModularArithmeticTheorems.v | |
| parent | 426f04e98c497feaed59b6604cc78ec5888077fc (diff) | |
prove admit about F.to_nat x mod m
Diffstat (limited to 'src/ModularArithmetic/ModularArithmeticTheorems.v')
| -rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 7 |
1 files changed, 7 insertions, 0 deletions
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. |