diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 18:33:25 +0100 |
commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /plugins/setoid_ring/Ring_theory.v | |
parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) |
Imported Upstream version 8.6
Diffstat (limited to 'plugins/setoid_ring/Ring_theory.v')
-rw-r--r-- | plugins/setoid_ring/Ring_theory.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index 7fcd6c08..f7757a18 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -238,7 +238,6 @@ Section ALMOST_RING. Variable req : R -> R -> Prop. Notation "0" := rO. Notation "1" := rI. Infix "==" := req. Infix "+" := radd. Infix "* " := rmul. - Infix "-" := rsub. Notation "- x" := (ropp x). (** Leibniz equality leads to a setoid theory and is extensional*) Lemma Eqsth : Equivalence (@eq R). @@ -263,7 +262,7 @@ Section ALMOST_RING. -x = x and x - y = x + y *) Definition SRopp (x:R) := x. Notation "- x" := (SRopp x). - Definition SRsub x y := x + -y. Notation "x - y " := (SRsub x y). + Definition SRsub x y := x + -y. Infix "-" := SRsub. Lemma SRopp_ext : forall x y, x == y -> -x == -y. Proof. intros x y H; exact H. Qed. @@ -320,6 +319,8 @@ Section ALMOST_RING. Qed. End SEMI_RING. + Infix "-" := rsub. + Notation "- x" := (ropp x). Variable Reqe : ring_eq_ext radd rmul ropp req. Add Morphism radd : radd_ext2. exact (Radd_ext Reqe). Qed. |