*** empty log message ***

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

2 files changed, 56 insertions, 54 deletions

diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 6ef0755022..86c1e124b9 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -373,14 +373,6 @@ Intros; Unfold cos_lb cos_ub; Apply (cos_bound a (S O) H H0).
 Qed.
 
 (**********)
-Lemma PI4_RGT_0 : ``0<PI/4``.
-Unfold Rdiv; Apply Rmult_lt_pos; [Apply PI_RGT_0 | Apply Rlt_Rinv; Sup0].
-Qed.
-
-Lemma PI6_RGT_0 : ``0<PI/6``.
-Unfold Rdiv; Apply Rmult_lt_pos; [Apply PI_RGT_0 | Apply Rlt_Rinv; Sup0].
-Qed.
-
 Lemma _PI2_RLT_0 : ``-(PI/2)<0``.
 Rewrite <- Ropp_O; Apply Rlt_Ropp1; Apply PI2_RGT_0.
 Qed.
@@ -394,15 +386,6 @@ Pattern 1 ``2``; Rewrite <- Rplus_Or.
 Replace ``4`` with ``2+2``; [Apply Rlt_compatibility; Apply Rgt_2_0 | Ring].
 Qed.
 
-Lemma PI6_RLT_PI2 : ``PI/6<PI/2``.
-Unfold Rdiv; Apply Rlt_monotony.
-Apply PI_RGT_0.
-Apply Rinv_lt.
-Apply Rmult_lt_pos; Sup0.
-Pattern 1 ``2``; Rewrite <- Rplus_Or.
-Replace ``6`` with ``2+4``; [Apply Rlt_compatibility; Sup0 | Ring].
-Qed.
-
 Lemma PI2_Rlt_PI : ``PI/2<PI``.
 Unfold Rdiv; Pattern 2 PI; Rewrite <- Rmult_1r.
 Apply Rlt_monotony.
@@ -880,26 +863,7 @@ Lemma tan_incr_1 : (x,y:R) ``-(PI/4)<=x``->``x<=PI/4`` ->``-(PI/4)<=y``->``y<=PI
 Intros; Case (total_order x y); Intro H4; [Left; Apply (tan_increasing_1 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_order (tan x) (tan y)); Intro H6; [Left; Assumption | Elim H6; Intro H7; [Right; Assumption | Generalize (tan_increasing_0 y x H1 H2 H H0 H7); Intro H8; Rewrite H5 in H8; Elim (Rlt_antirefl y H8)]] | Elim (Rlt_antirefl x (Rle_lt_trans x y x H3 H5))]].
 Qed.
 
-Lemma Rgt_3PI2_0 : ``0<3*(PI/2)``.
-Apply Rmult_lt_pos; [Apply Rgt_3_0 | Unfold Rdiv; Apply Rmult_lt_pos; [Apply PI_RGT_0 | Apply Rlt_Rinv; Apply Rgt_2_0]].
-Qed.
-  
-Lemma Rgt_2PI_0 : ``0<2*PI``.
-Apply Rmult_lt_pos; [Apply Rgt_2_0 | Apply PI_RGT_0].
-Qed.
-
-Lemma Rlt_PI_3PI2 : ``PI<3*(PI/2)``.
-Generalize PI2_RGT_0; Intro H1; Generalize (Rlt_compatibility PI ``0`` ``PI/2`` H1); Replace ``PI+(PI/2)`` with ``3*(PI/2)``.
-Rewrite Rplus_Or; Intro H2; Assumption.
-Pattern 2 PI; Rewrite double_var; Ring.
-Qed. 
- 
-Lemma Rlt_3PI2_2PI : ``3*(PI/2)<2*PI``.
-Generalize PI2_RGT_0; Intro H1; Generalize (Rlt_compatibility ``3*(PI/2)`` ``0`` ``PI/2`` H1); Replace ``3*(PI/2)+(PI/2)`` with ``2*PI``.
-Rewrite Rplus_Or; Intro H2; Assumption.
-Rewrite double; Pattern 1 2 PI; Rewrite double_var; Ring.
-Qed.
-
+(**********)
 Lemma sin_eq_0_1 : (x:R) (EXT k:Z | x==(Rmult (IZR k) PI)) -> (sin x)==R0.
 Intros.
 Elim H; Intros.
@@ -1178,21 +1142,4 @@ Qed.
 
 Lemma  cos_eq_0_2PI_1 : (x:R) ``0<=x`` -> ``x<=2*PI`` -> ``x==PI/2``\/``x==3*(PI/2)`` -> ``(cos x)==0``.
 Intros x H1 H2 H3; Elim H3; Intro H4; [ Rewrite H4; Rewrite -> cos_PI2; Reflexivity | Rewrite H4; Rewrite -> cos_3PI2; Reflexivity ].
-Qed.
-
-(***************************************************)
-(*                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 sum_f_R0; 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)).
 Qed.
\ No newline at end of file
diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v
index af6c6d59e0..ff44bd7b36 100644
--- a/theories/Reals/Rtrigo_calc.v
+++ b/theories/Reals/Rtrigo_calc.v
@@ -10,6 +10,7 @@
 
 Require Rbase.
 Require DiscrR.
+Require Rseries.
 Require R_sqr.
 Require Rlimit.
 Require Rtrigo.
@@ -108,6 +109,19 @@ Rewrite Rmult_1r; Reflexivity.
 DiscrR.
 Qed.
 
+Lemma PI6_RGT_0 : ``0<PI/6``.
+Unfold Rdiv; Apply Rmult_lt_pos; [Apply PI_RGT_0 | Apply Rlt_Rinv; Sup0].
+Qed.
+
+Lemma PI6_RLT_PI2 : ``PI/6<PI/2``.
+Unfold Rdiv; Apply Rlt_monotony.
+Apply PI_RGT_0.
+Apply Rinv_lt.
+Apply Rmult_lt_pos; Sup0.
+Pattern 1 ``2``; Rewrite <- Rplus_Or.
+Replace ``6`` with ``2+4``; [Apply Rlt_compatibility; Sup0 | Ring].
+Qed.
+
 Lemma sin_PI6 : ``(sin (PI/6))==1/2``.
 Apply r_Rmult_mult with ``2*(cos (PI/6))``.
 Replace ``2*(cos (PI/6))*(sin (PI/6))`` with ``2*(sin (PI/6))*(cos (PI/6))``.
@@ -158,6 +172,10 @@ Lemma Rlt_sqrt3_0 : ``0<(sqrt 3)``.
 Cut ~(O=(1)); [Intro H0; Generalize (Rlt_le ``0`` ``2`` Rgt_2_0); Intro H1; Generalize (Rlt_le ``0`` ``3`` Rgt_3_0); Intro H2; Generalize (lt_INR_0 (1) (neq_O_lt (1) H0)); Unfold INR; Intro H3; Generalize (Rlt_compatibility ``2`` ``0`` ``1`` H3); Rewrite Rplus_sym; Rewrite Rplus_Ol; Replace ``2+1`` with ``3``; [Intro H4; Generalize (sqrt_lt_1 ``2`` ``3`` H1 H2 H4); Clear H3; Intro H3; Apply (Rlt_trans ``0`` ``(sqrt 2)`` ``(sqrt 3)`` Rlt_sqrt2_0 H3) | Ring] | Discriminate].
 Qed.
 
+Lemma PI4_RGT_0 : ``0<PI/4``.
+Unfold Rdiv; Apply Rmult_lt_pos; [Apply PI_RGT_0 | Apply Rlt_Rinv; Sup0].
+Qed.
+
 Lemma cos_PI4 : ``(cos (PI/4))==1/(sqrt 2)``.
 Apply Rsqr_inj.
 Apply cos_ge_0.
@@ -439,6 +457,26 @@ Lemma sin_cos5PI4 : ``(cos (5*(PI/4)))==(sin (5*(PI/4)))``.
 Rewrite cos_5PI4; Rewrite sin_5PI4; Reflexivity.
 Qed.
 
+Lemma Rgt_3PI2_0 : ``0<3*(PI/2)``.
+Apply Rmult_lt_pos; [Apply Rgt_3_0 | Unfold Rdiv; Apply Rmult_lt_pos; [Apply PI_RGT_0 | Apply Rlt_Rinv; Apply Rgt_2_0]].
+Qed.
+
+Lemma Rgt_2PI_0 : ``0<2*PI``.
+Apply Rmult_lt_pos; [Apply Rgt_2_0 | Apply PI_RGT_0].
+Qed.
+
+Lemma Rlt_PI_3PI2 : ``PI<3*(PI/2)``.
+Generalize PI2_RGT_0; Intro H1; Generalize (Rlt_compatibility PI ``0`` ``PI/2`` H1); Replace ``PI+(PI/2)`` with ``3*(PI/2)``.
+Rewrite Rplus_Or; Intro H2; Assumption.
+Pattern 2 PI; Rewrite double_var; Ring.
+Qed. 
+ 
+Lemma Rlt_3PI2_2PI : ``3*(PI/2)<2*PI``.
+Generalize PI2_RGT_0; Intro H1; Generalize (Rlt_compatibility ``3*(PI/2)`` ``0`` ``PI/2`` H1); Replace ``3*(PI/2)+(PI/2)`` with ``2*PI``.
+Rewrite Rplus_Or; Intro H2; Assumption.
+Rewrite double; Pattern 1 2 PI; Rewrite double_var; Ring.
+Qed.
+
 (***************************************************************)
 (* Radian -> Degree | Degree -> Radian                         *)
 (***************************************************************)
@@ -484,4 +522,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.
+Qed.
+
+(***************************************************)
+(*                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 sum_f_R0; 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)).
 Qed.
\ No newline at end of file