diff options
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. |