diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-04-25 17:37:05 -0400 |
|---|---|---|
| committer |  Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:44:46 -0400 |
| commit | ddb2d8ad8c765ce03d296e76e4e0855977131f08 (patch) | |
| tree | 46085ee6647699335129c40c9105062a0c7708d9 /src/ModularArithmetic/ModularArithmeticTheorems.v | |
| parent | 37e2a9e80607eb8771aea1b371f464a8d7ce8464 (diff) | |
refactor field lemmas out of ed25519
Diffstat (limited to 'src/ModularArithmetic/ModularArithmeticTheorems.v')
| -rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index ddb689547..954fac15d 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -513,6 +513,11 @@ Section VariousModulo. ring. Qed. + Lemma F_opp_0 : opp (0 : F m) = 0%F. + Proof. + intros; ring. + Qed. + Lemma F_opp_swap : forall x y : F m, opp x = y <-> x = opp y. Proof. split; intro; subst; ring. @@ -523,6 +528,23 @@ Section VariousModulo. intros; ring. Qed. + Lemma F_square_opp : forall x : F m, (opp x ^ 2 = x ^ 2)%F. + Proof. + intros; ring. + Qed. + + Lemma F_mul_opp_r : forall x y : F m, (x * opp y = opp (x * y))%F. + intros; ring. + Qed. + + Lemma F_mul_opp_l : forall x y : F m, (opp x * y = opp (x * y))%F. + intros; ring. + Qed. + + Lemma F_mul_opp_both : forall x y : F m, (opp x * opp y = x * y)%F. + intros; ring. + Qed. + Lemma F_add_0_r : forall x : F m, (x + 0)%F = x. Proof. intros; ring. |