diff options
Diffstat (limited to 'src/Algebra/Ring.v')
| -rw-r--r-- | src/Algebra/Ring.v | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v index 5c1cb1603..2b0e1ba80 100644 --- a/src/Algebra/Ring.v +++ b/src/Algebra/Ring.v @@ -1,8 +1,13 @@ +Require Coq.setoid_ring.Ncring. +Require Coq.setoid_ring.Cring. Require Import Coq.Classes.Morphisms. -Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.OnSubterms. +Require Import Crypto.Util.Tactics.Revert. Require Import Crypto.Algebra Crypto.Algebra.Group Crypto.Algebra.Monoid. Require Coq.ZArith.ZArith Coq.PArith.PArith. + Section Ring. Context {T eq zero one opp add sub mul} `{@ring T eq zero one opp add sub mul}. Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. @@ -86,10 +91,6 @@ Section Ring. forall x y : T, not (eq (mul x y) zero) <-> (not (eq x zero) /\ not (eq y zero)). Proof. intros; rewrite zero_product_iff_zero_factor; tauto. Qed. - Lemma nonzero_hypothesis_to_goal {Hzpzf:@is_zero_product_zero_factor T eq zero mul} : - forall x y : T, (not (eq x zero) -> eq y zero) <-> (eq (mul x y) zero). - Proof. intros; rewrite zero_product_iff_zero_factor; tauto. Qed. - Global Instance Ncring_Ring_ops : @Ncring.Ring_ops T zero one add mul sub opp eq. Global Instance Ncring_Ring : @Ncring.Ring T zero one add mul sub opp eq Ncring_Ring_ops. Proof. @@ -434,4 +435,4 @@ Create HintDb ring_simplify_subterms discriminated. Create HintDb ring_simplify_subterms_in_all discriminated. Hint Extern 1 => progress ring_simplify : ring_simplify. Hint Extern 1 => progress ring_simplify_subterms : ring_simplify_subterms. -Hint Extern 1 => progress ring_simplify_subterms_in_all : ring_simplify_subterms_in_all.
\ No newline at end of file +Hint Extern 1 => progress ring_simplify_subterms_in_all : ring_simplify_subterms_in_all. |