*** empty log message ***

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

3 files changed, 44 insertions, 1 deletions

diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v
index 19ac6d97b6..c6596c5883 100644
--- a/theories/Reals/R_sqr.v
+++ b/theories/Reals/R_sqr.v
@@ -49,6 +49,14 @@ Lemma Rsqr_eq_0 : (x:R) ``(Rsqr x)==0`` -> ``x==0``.
 Unfold Rsqr; Intros; Generalize (without_div_Od x x H); Intro; Elim H0; Intro ; Assumption.
 Save.
 
+Lemma Rsqr_minus_plus : (a,b:R) ``(a-b)*(a+b)==(Rsqr a)-(Rsqr b)``.
+Intros; SqRing.
+Save.
+
+Lemma Rsqr_plus_minus : (a,b:R) ``(a+b)*(a-b)==(Rsqr a)-(Rsqr b)``.
+Intros; SqRing.
+Save.
+
 Lemma Rsqr_incr_0 : (x,y:R) ``(Rsqr x)<=(Rsqr y)`` -> ``0<=x`` -> ``0<=y`` -> ``x<=y``.
 Intros; Case (total_order_Rle x y); Intro; [Assumption | Cut ``y<x``; [Intro; Unfold Rsqr in H; Generalize (Rmult_lt2 y x y x H1 H1 H2 H2); Intro; Generalize (Rle_lt_trans ``x*x`` ``y*y`` ``x*x`` H H3); Intro; Elim (Rlt_antirefl ``x*x`` H4) | Auto with real]].
 Save.
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index 482cfa0cc0..d24520e777 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -1567,6 +1567,24 @@ Lemma Rmult_lt2 : (r1,r2,r3,r4:R) ``0<=r1`` -> ``0<=r3`` -> ``r1<r2`` -> ``r3<r4
 Intros; Apply Rle_lt_trans with ``r2*r3``; [Apply Rle_monotony_r; [Assumption | Left; Assumption] | Apply Rlt_monotony; [Apply Rle_lt_trans with r1; Assumption | Assumption]].
 Save.
 
+Lemma le_epsilon : (x,y:R) ((eps : R) ``0<eps``->``x<=y+eps``) -> ``x<=y``.
+Intros; Elim (total_order x y); Intro.
+Left; Assumption.
+Elim H0; Intro.
+Right; Assumption.
+Clear H0; Generalize (Rgt_minus x y H1); Intro H2; Change ``0<x-y`` in H2.
+Cut ``0<2``.
+Intro.
+Generalize (Rmult_lt_pos ``x-y`` ``/2`` H2 (Rlt_Rinv ``2`` H0)); Intro H3; Generalize (H ``(x-y)*/2`` H3); Replace ``y+(x-y)*/2`` with ``(y+x)*/2``.
+Intro H4; Generalize (Rle_monotony ``2`` x ``(y+x)*/2`` (Rlt_le ``0`` ``2`` H0) H4); Rewrite <- (Rmult_sym ``((y+x)*/2)``); Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Replace ``2*x`` with ``x+x``.
+Rewrite (Rplus_sym y); Intro H5; Apply Rle_anti_compatibility with x; Assumption.
+Ring. 
+Replace ``2`` with (INR (S (S O))); [Apply not_O_INR; Discriminate | Ring].
+Field; Replace ``2`` with (INR (S (S O))); [Apply not_O_INR; Discriminate | Ring].
+Cut ~(O=(2)); [Intro H0; Generalize (lt_INR_0 (2) (neq_O_lt (2) H0)); Unfold INR; Intro; Assumption | Discriminate].
+Save.
+
 (*****************************************************)
 (* Résultat complémentaire sur la fonction INR       *)
 (*****************************************************)
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index bc7892207e..4b147eac20 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -888,4 +888,21 @@ Definition tand [x:R] : R := (tan (toRad x)).
 
 Lemma Rsqr_sin_cos_d_one : (x:R) ``(Rsqr (sind x))+(Rsqr (cosd x))==1``.
 Intro x; Unfold sind; Unfold cosd; Apply sin2_cos2.
-Save.
\ No newline at end of file
+Save.
+
+(***************************************************)
+(*                Other properties                 *)
+(***************************************************)
+
+Lemma sin_lb_ge_0 : (a:R) ``0<=a``->``a<=PI/2``->``0<=(sin_lb a)``.
+Intros; Case (total_order R0 a); Intro.
+Left; Apply sin_lb_gt_0; Assumption.
+Elim H1; Intro.
+Rewrite <- H2; Unfold sin_lb; Unfold sin_approx; Unfold sigma_aux; Unfold sin_term; Repeat Rewrite pow_ne_zero.
+Unfold Rdiv; Repeat Rewrite Rmult_Ol; Repeat Rewrite Rmult_Or; Repeat Rewrite Rplus_Or; Right; Reflexivity.
+Simpl; Discriminate.
+Simpl; Discriminate.
+Simpl; Discriminate.
+Simpl; Discriminate.
+Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` a ``0`` H H2)).
+Save.