Ajout tactics Reals

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

1 files changed, 25 insertions, 1 deletions

diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index 4b4ab6351..f8b88f9c6 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -492,12 +492,22 @@ Intro;Ring.
 Save.
 Hints Resolve minus_R0 : real.
 
+Lemma Rminus_Ropp:(r:R)``0-r==-r``.
+Intro;Ring.
+Save.
+Hints Resolve Rminus_Ropp : real.
+
 (**********)
 Lemma Ropp_distr2:(r1,r2:R)``-(r1-r2)==r2-r1``.
   Intros; Ring.
 Save.
 Hints Resolve Ropp_distr2 : real.
 
+Lemma Ropp_distr3:(r1,r2:R)``-(r2-r1)==r1-r2``.
+Intros; Ring.
+Save.
+Hints Resolve Ropp_distr3 : real. 
+
 (**********)
 Lemma eq_Rminus:(r1,r2:R)(r1==r2)->``r1-r2==0``.
   Intros; Rewrite H; Ring.
@@ -511,6 +521,11 @@ Lemma Rminus_eq:(r1,r2:R)``r1-r2==0`` -> r1==r2.
 Save.
 Hints Immediate Rminus_eq : real.
 
+Lemma Rminus_eq_right:(r1,r2:R)``r2-r1==0`` -> r1==r2.
+Intros;Generalize (Rminus_eq r2 r1 H);Clear H;Intro H;Rewrite H;Ring.
+Save.
+Hints Immediate Rminus_eq_right : real.
+
 (**********)
 Lemma Rminus_eq_contra:(r1,r2:R)``r1<>r2``->``r1-r2<>0``.
 Red; Intros r1 r2 H H0.
@@ -518,6 +533,16 @@ Apply H; Auto with real.
 Save.
 Hints Resolve Rminus_eq_contra : real.
 
+Lemma Rminus_not_eq:(r1,r2:R)``r1-r2<>0``->``r1<>r2``.
+Red; Intros; Elim H; Apply eq_Rminus; Auto.
+Save.
+Hints Resolve Rminus_not_eq : real.
+
+Lemma Rminus_not_eq_right:(r1,r2:R)``r2-r1<>0`` -> ``r1<>r2``.
+Red; Intros;Elim H;Rewrite H0; Ring.
+Save.
+Hints Resolve Rminus_not_eq_right : real. 
+
 (**********)
 Lemma Rminus_distr:  (x,y,z:R) ``x*(y-z)==(x*y) - (x*z)``.
 Intros; Ring.
@@ -752,7 +777,6 @@ Lemma Rmult_lt:(r1,r2,r3,r4:R)``r3>0`` -> ``r2>0`` ->
 Intros; Apply Rlt_trans with ``r2*r3``; Auto with real.
 Save.
 
-
 (*s Order and Substractions *)
 Lemma Rlt_minus:(r1,r2:R)``r1 < r2`` -> ``r1-r2 < 0``.
 Intros; Apply (Rlt_anti_compatibility ``r2``).