diff options
| author | herbelin | 2003-05-21 13:59:36 +0000 |
|---|---|---|
| committer | herbelin | 2003-05-21 13:59:36 +0000 |
| commit | 9e2ba1d42bfeff9aafc8384fb131330b725ce3be (patch) | |
| tree | 5e4c6a613580cec0230ba83471686506352eaf1d /contrib | |
| parent | 6fe9381c21e6700791318920afd656a22c6a32b5 (diff) | |
Concentration des notations officielles dans Init/Notations; restructuration de Init
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4050 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/ring/Ring_theory.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v index 08bb53955e..1f6b614eb2 100644 --- a/contrib/ring/Ring_theory.v +++ b/contrib/ring/Ring_theory.v @@ -306,7 +306,7 @@ Lemma Th_plus_opp_opp : (x,y:A) (-x) + (-y) == -(x+y). Intros. Apply (aux2 1! x + y); [ Elim plus_assoc; - Rewrite -> (Th_plus_permute y -x); Rewrite -> plus_assoc; + Rewrite -> (Th_plus_permute y (-x)); Rewrite -> plus_assoc; Rewrite -> opp_def; Rewrite plus_zero_left; Auto | Auto ]. Qed. @@ -331,13 +331,13 @@ Lemma Th_mult_opp_opp2 : (x,y:A) x*y == (-x)*(-y). Symmetry; Apply Th_mult_opp_opp. Qed. Lemma Th_opp_zero : -0 == 0. -Rewrite <- (plus_zero_left -0). +Rewrite <- (plus_zero_left (-0)). Auto. Qed. Lemma Th_plus_reg_left : (n,m,p:A) n + m == n + p -> m==p. Intros; Generalize (congr_eqT ? ? [z] (-n)+z ? ? H). Repeat Rewrite plus_assoc. -Rewrite (plus_sym -n n). +Rewrite (plus_sym (-n) n). Rewrite opp_def. Repeat Rewrite Th_plus_zero_left; EAuto. Qed. |