diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-09-21 20:45:01 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-09-22 10:44:07 -0400 |
| commit | 5357fe92e65712a3e2506fe0a939b358d14183d7 (patch) | |
| tree | ea0328c53e10620d9a46cd13606a5b6646ce7d6f /src/ModularArithmetic | |
| parent | fd5cba50d8743149e7ca4e386716126f2fc03e63 (diff) | |
alternative signing derivation
cleanup
Diffstat (limited to 'src/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 5984b4e6d..f1a2d15a4 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -173,6 +173,14 @@ Module F. rewrite Z2Nat.id by omega. rewrite <-F.of_Z_mod; reflexivity. 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. + + Lemma of_nat_mul 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_mul, F.of_Z_mul; reflexivity. Qed. End FandNat. Section RingTacticGadgets. |