Modif de l'axiomatisation pour enlever les /\ de _ne

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1278 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 13 deletions

diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index f2f6cc2d7..1fb31101d 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -19,8 +19,8 @@ Lemma RTheory : (Ring_Theory Rplus Rmult R1 R0 Ropp [x,y:R]false).
   Symmetry; Apply Rplus_assoc.
   Exact Rmult_sym.
   Symmetry; Apply Rmult_assoc.
-  Intro; Apply (let (H1,H2)=(Rplus_ne n) in H2).
-  Intro; Apply (let (H1,H2)=(Rmult_ne n) in H2).
+  Intro; Apply Rplus_Ol.
+  Intro; Apply Rmult_1l.
   Exact Rplus_Ropp_r.
   Intros.
   Rewrite Rmult_sym.
@@ -253,16 +253,15 @@ Save.
 (*s      Addition                                        *)
 (*********************************************************)
 
-Lemma Rplus_Or:(r:R)``r+0==r``.
-Intro; Ring.
+Lemma Rplus_ne:(r:R)``r+0==r``/\``0+r==r``.
+Intro;Split;Ring.
 Save.
-Hints Resolve Rplus_Or : real.
+Hints Resolve Rplus_ne : real v62.
 
-(**********)
-Lemma Rplus_Ol:(r:R)``0+r==r``.
+Lemma Rplus_Or:(r:R)``r+0==r``.
 Intro; Ring.
 Save.
-Hints Resolve Rplus_Ol : real.
+Hints Resolve Rplus_Or : real.
 
 (**********)
 Lemma Rplus_Ropp_l:(r:R)``(-r)+r==0``.
@@ -335,16 +334,16 @@ Save.
 Hints Resolve Rmult_Ol : real v62.
 
 (**********)
-Lemma Rmult_1r:(r:R)(``r*1==r``).
-Intro; Ring.
+Lemma Rmult_ne:(r:R)``r*1==r``/\``1*r==r``.
+Intro;Split;Ring.
 Save.
-Hints Resolve Rmult_1r : real.
+Hints Resolve Rmult_ne : real v62.
 
 (**********)
-Lemma Rmult_1l:(r:R)(``1*r==r``).
+Lemma Rmult_1r:(r:R)(``r*1==r``).
 Intro; Ring.
 Save.
-Hints Resolve Rmult_1l : real.
+Hints Resolve Rmult_1r : real.
 
 (**********)
 Lemma Rmult_mult_r:(r,r1,r2:R)r1==r2->``r*r1==r*r2``.