*** empty log message ***

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

3 files changed, 21 insertions, 38 deletions

diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v
index fec2f93d73..39cca741c4 100644
--- a/theories/Reals/R_sqr.v
+++ b/theories/Reals/R_sqr.v
@@ -54,7 +54,7 @@ Intros; Case (total_order_Rle x y); Intro; [Assumption | Cut ``y<x``; [Intro; Un
 Save.
 
 Lemma Rsqr_incr_1 : (x,y:R) ``x<=y``->``0<=x``->``0<= y``->``(Rsqr x)<=(Rsqr y)``.
-Intros; Unfold Rsqr; Apply Rmult_le; Assumption.
+Intros; Unfold Rsqr; Apply Rle_Rmult_comp; Assumption.
 Save.
 
 Lemma Rsqr_incrst_0 : (x,y:R) ``(Rsqr x)<(Rsqr y)``->``0<=x``->``0<=y``-> ``x<y``.
@@ -187,7 +187,7 @@ Intros x H1; Unfold Rsqr; Apply (bar x H1).
 Save.
 
 Lemma sqrt_times : (x,y:R) ``0<=x``->``0<=y``->``(sqrt (x*y))==(sqrt x)*(sqrt y)``.
-Intros x y H1 H2; Apply (Rsqr_inj (sqrt (Rmult x y)) (Rmult (sqrt x) (sqrt y)) (foo (Rmult x y) (regle_signe_le x y H1 H2)) (regle_signe_le (sqrt x) (sqrt y) (foo x H1) (foo y H2))); Rewrite Rsqr_times; Repeat Rewrite Rsqr_sqrt; [Ring | Assumption |Assumption | Apply (regle_signe_le x y H1 H2)].
+Intros x y H1 H2; Apply (Rsqr_inj (sqrt (Rmult x y)) (Rmult (sqrt x) (sqrt y)) (foo (Rmult x y) (Rmult_le_pos x y H1 H2)) (Rmult_le_pos (sqrt x) (sqrt y) (foo x H1) (foo y H2))); Rewrite Rsqr_times; Repeat Rewrite Rsqr_sqrt; [Ring | Assumption |Assumption | Apply (Rmult_le_pos x y H1 H2)].
 Save.
 
 Lemma sqrt_lt_R0 : (x:R) ``0<x`` -> ``0<(sqrt x)``.
@@ -195,7 +195,7 @@ Intros x H1; Apply Rsqr_incrst_0; [Rewrite Rsqr_O; Rewrite Rsqr_sqrt ; [Assumpti
 Save.
 
 Lemma sqrt_div : (x,y:R) ``0<=x``->``0<y``->``(sqrt (x/y))==(sqrt x)/(sqrt y)``.
-Intros x y H1 H2; Apply Rsqr_inj; [ Apply foo; Apply (regle_signe_le x (Rinv y)); [ Assumption | Generalize (Rlt_Rinv y H2); Clear H2; Intro H2; Left; Assumption] | Apply (regle_signe_le (sqrt x) (Rinv (sqrt y))) ; [ Apply (foo x H1) | Generalize (sqrt_lt_R0 y H2); Clear H2; Intro H2; Generalize (Rlt_Rinv (sqrt y) H2); Clear H2; Intro H2; Left; Assumption] | Rewrite Rsqr_div; Repeat Rewrite Rsqr_sqrt; [ Reflexivity | Left; Assumption | Assumption | Generalize (Rlt_Rinv y H2); Intro H3; Generalize (Rlt_le R0 (Rinv y) H3); Intro H4; Apply (regle_signe_le x (Rinv y) H1 H4) |Red; Intro H3; Generalize (Rlt_le R0 y H2); Intro H4; Generalize (sqrt_eq_0 y H4 H3); Intro H5; Rewrite H5 in H2; Elim (Rlt_antirefl R0 H2)]].
+Intros x y H1 H2; Apply Rsqr_inj; [ Apply foo; Apply (Rmult_le_pos x (Rinv y)); [ Assumption | Generalize (Rlt_Rinv y H2); Clear H2; Intro H2; Left; Assumption] | Apply (Rmult_le_pos (sqrt x) (Rinv (sqrt y))) ; [ Apply (foo x H1) | Generalize (sqrt_lt_R0 y H2); Clear H2; Intro H2; Generalize (Rlt_Rinv (sqrt y) H2); Clear H2; Intro H2; Left; Assumption] | Rewrite Rsqr_div; Repeat Rewrite Rsqr_sqrt; [ Reflexivity | Left; Assumption | Assumption | Generalize (Rlt_Rinv y H2); Intro H3; Generalize (Rlt_le R0 (Rinv y) H3); Intro H4; Apply (Rmult_le_pos x (Rinv y) H1 H4) |Red; Intro H3; Generalize (Rlt_le R0 y H2); Intro H4; Generalize (sqrt_eq_0 y H4 H3); Intro H5; Rewrite H5 in H2; Elim (Rlt_antirefl R0 H2)]].
 Save.
 
 Lemma sqrt_lt_0 : (x,y:R) ``0<=x``->``0<=y``->``(sqrt x)<(sqrt y)``->``x<y``.
@@ -229,7 +229,7 @@ Intros x H1 H2; Generalize (sqrt_lt_1 x R1 (Rlt_le R0 x H1) (Rlt_le R0 R1 (Rlt_R
 Save.
 
 Lemma sqrt_cauchy : (a,b,c,d:R) ``a*c+b*d<=(sqrt ((Rsqr a)+(Rsqr b)))*(sqrt ((Rsqr c)+(Rsqr d)))``.
-Intros a b c d; Apply Rsqr_incr_0_var; [Rewrite Rsqr_times; Repeat Rewrite Rsqr_sqrt; Unfold Rsqr; [Replace ``(a*c+b*d)*(a*c+b*d)`` with ``(a*a*c*c+b*b*d*d)+(2*a*b*c*d)``; [Replace ``(a*a+b*b)*(c*c+d*d)`` with ``(a*a*c*c+b*b*d*d)+(a*a*d*d+b*b*c*c)``; [Apply Rle_compatibility; Replace ``a*a*d*d+b*b*c*c`` with ``(2*a*b*c*d)+(a*a*d*d+b*b*c*c-2*a*b*c*d)``; [Pattern 1 ``2*a*b*c*d``; Rewrite <- Rplus_Or; Apply Rle_compatibility; Replace ``a*a*d*d+b*b*c*c-2*a*b*c*d`` with (Rsqr (Rminus (Rmult a d) (Rmult b c))); [Apply pos_Rsqr | Unfold Rsqr; Ring] | Ring] | Ring] | Ring] | Apply (ge0_plus_ge0_is_ge0 (Rsqr c) (Rsqr d) (pos_Rsqr c) (pos_Rsqr d)) | Apply (ge0_plus_ge0_is_ge0 (Rsqr a) (Rsqr b) (pos_Rsqr a) (pos_Rsqr b))] | Apply regle_signe_le; Apply foo; Apply ge0_plus_ge0_is_ge0; Apply pos_Rsqr].
+Intros a b c d; Apply Rsqr_incr_0_var; [Rewrite Rsqr_times; Repeat Rewrite Rsqr_sqrt; Unfold Rsqr; [Replace ``(a*c+b*d)*(a*c+b*d)`` with ``(a*a*c*c+b*b*d*d)+(2*a*b*c*d)``; [Replace ``(a*a+b*b)*(c*c+d*d)`` with ``(a*a*c*c+b*b*d*d)+(a*a*d*d+b*b*c*c)``; [Apply Rle_compatibility; Replace ``a*a*d*d+b*b*c*c`` with ``(2*a*b*c*d)+(a*a*d*d+b*b*c*c-2*a*b*c*d)``; [Pattern 1 ``2*a*b*c*d``; Rewrite <- Rplus_Or; Apply Rle_compatibility; Replace ``a*a*d*d+b*b*c*c-2*a*b*c*d`` with (Rsqr (Rminus (Rmult a d) (Rmult b c))); [Apply pos_Rsqr | Unfold Rsqr; Ring] | Ring] | Ring] | Ring] | Apply (ge0_plus_ge0_is_ge0 (Rsqr c) (Rsqr d) (pos_Rsqr c) (pos_Rsqr d)) | Apply (ge0_plus_ge0_is_ge0 (Rsqr a) (Rsqr b) (pos_Rsqr a) (pos_Rsqr b))] | Apply Rmult_le_pos; Apply foo; Apply ge0_plus_ge0_is_ge0; Apply pos_Rsqr].
 Save.
 
 (************************************************************)
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index b37b7b1a06..78e0876a02 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -1530,18 +1530,13 @@ Lemma prod_neq_R0 : (x,y:R) ~``x==0``->~``y==0``->~``x*y==0``.
 Intros; Red; Intro; Generalize (without_div_Od x y H1); Intro; Elim H2; Intro; [Rewrite H3 in H; Elim H | Rewrite H3 in H0; Elim H0]; Reflexivity.
 Save.
 
-(**********)
-Lemma regle_signe : (x,y:R) ``0<x`` -> ``0<y`` -> ``0<x*y``.
-Intros; Rewrite <- (Rmult_Ol x); Rewrite <- (Rmult_sym x); Apply (Rlt_monotony x R0 y H H0).
-Save.
-
 (*********)
-Lemma regle_signe_le : (x,y:R) ``0<=x`` -> ``0<=y`` -> ``0<=x*y``.
+Lemma Rmult_le_pos : (x,y:R) ``0<=x`` -> ``0<=y`` -> ``0<=x*y``.
 Intros; Rewrite <- (Rmult_Ol x); Rewrite <- (Rmult_sym x); Apply (Rle_monotony x R0 y H H0).
 Save.
 
 (**********************************************************)
-(* Quelques règles concernant < et <=                     *)
+(* Other rules about < and <=                             *)
 (**********************************************************)
 
 Lemma gt0_plus_gt0_is_gt0 : (x,y:R) ``0<x`` -> ``0<y`` -> ``0<x+y``.
@@ -1560,22 +1555,10 @@ Lemma ge0_plus_ge0_is_ge0 : (x,y:R) ``0<=x`` -> ``0<=y`` -> ``0<=x+y``.
 Intros; Apply Rle_trans with x; [Assumption | Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Assumption].
 Save.
 
-Lemma ge0_plus_ge0_eq_0 : (x,y:R) ``0<=x`` -> ``0<=y`` -> ``x+y==0`` -> ``x==0``/\``y==0``.
-Intros; Split; [Elim H; Intro; [Generalize (gt0_plus_ge0_is_gt0 x y H2 H0); Intro; Rewrite H1 in H3; Elim (Rlt_antirefl ``0`` H3) | Symmetry; Assumption] | Elim H0; Intro; [Generalize (ge0_plus_gt0_is_gt0 x y H H2); Intro; Rewrite H1 in H3; Elim (Rlt_antirefl R0 H3) | Symmetry; Assumption]].
-Save.
-
-Lemma Rmult_le : (r1,r2,r3,r4:R) ``0<=r1`` -> ``0<=r3`` -> ``r1<=r2`` -> ``r3<=r4`` -> ``r1*r3<=r2*r4``.
-Intros; Apply Rle_trans with ``r2*r3``; [Apply Rle_monotony_r; Assumption | Apply Rle_monotony; [ Apply Rle_trans with r1; Assumption | Assumption]].
-Save.
-
 Lemma plus_le_is_le : (x,y,z:R) ``0<=y`` -> ``x+y<=z`` -> ``x<=z``.
 Intros; Apply Rle_trans with ``x+y``; [Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Assumption | Assumption].
 Save.
 
-Lemma le_plus_lt_is_lt : (x,y,z,t:R) ``x<=y`` -> ``z<t`` -> ``x+z<y+t``. 
-Intros; Apply Rle_lt_trans with ``y+z``; [Apply Rle_compatibility_r; Assumption | Apply Rlt_compatibility; Assumption].
-Save.
-
 Lemma plus_lt_is_lt : (x,y,z:R) ``0<=y`` -> ``x+y<z`` -> ``x<z``.
 Intros; Apply Rle_lt_trans with ``x+y``; [Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Assumption | Assumption].
 Save.
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 5875ede76f..f3d9d26efd 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -14,7 +14,7 @@ Definition PI_ub : R := ``315/100``.
 Axiom PI_approx : ``PI_lb <= PI <= PI_ub``.
 
 Lemma PI_neq0 : ~``PI==0``.
-Red; Intro H1; Generalize PI_approx; Intro H2; Elim H2; Intros H3 H4; Rewrite H1 in H3; Unfold PI_lb in H3; Cut ~(O=(314)); [Intro; Generalize (lt_INR_0 (314) (neq_O_lt (314) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H5; Cut ~(O=(100)); [Intro; Generalize (lt_INR_0 (100) (neq_O_lt (100) H0)); Rewrite INR_eq_INR2; Unfold INR2; Intro H6; Generalize (Rlt_Rinv ``100`` H6); Intro H7; Generalize (regle_signe ``314`` (Rinv ``100``) H5 H7); Intro H8; Generalize (Rle_lt_trans ``314/100`` R0 ``314/100`` H3 H8); Intro H9; Elim (Rlt_antirefl ``314/100`` H9) | Discriminate] | Discriminate].
+Red; Intro H1; Generalize PI_approx; Intro H2; Elim H2; Intros H3 H4; Rewrite H1 in H3; Unfold PI_lb in H3; Cut ~(O=(314)); [Intro; Generalize (lt_INR_0 (314) (neq_O_lt (314) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H5; Cut ~(O=(100)); [Intro; Generalize (lt_INR_0 (100) (neq_O_lt (100) H0)); Rewrite INR_eq_INR2; Unfold INR2; Intro H6; Generalize (Rlt_Rinv ``100`` H6); Intro H7; Generalize (Rmult_lt_pos ``314`` (Rinv ``100``) H5 H7); Intro H8; Generalize (Rle_lt_trans ``314/100`` R0 ``314/100`` H3 H8); Intro H9; Elim (Rlt_antirefl ``314/100`` H9) | Discriminate] | Discriminate].
 Save.
 
 (******************************************************************)
@@ -252,7 +252,7 @@ Save.
 Lemma PI_RGT_0 : ``0<PI``.
 Cut ~(O=(314)).
 Cut ~(O=(100)).
-Intros; Apply Rlt_le_trans with PI_lb; [Unfold PI_lb; Generalize (lt_INR_0 (314) (neq_O_lt (314) H0)); Rewrite INR_eq_INR2; Unfold INR2; Intro H1; Generalize (lt_INR_0 (100) (neq_O_lt (100) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H2; Generalize (Rlt_Rinv ``100`` H2); Intro H3; Generalize (regle_signe ``314`` (Rinv ``100``) H1 H3); Intro H4 | Elim PI_approx; Intros H3 _]; Assumption.
+Intros; Apply Rlt_le_trans with PI_lb; [Unfold PI_lb; Generalize (lt_INR_0 (314) (neq_O_lt (314) H0)); Rewrite INR_eq_INR2; Unfold INR2; Intro H1; Generalize (lt_INR_0 (100) (neq_O_lt (100) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H2; Generalize (Rlt_Rinv ``100`` H2); Intro H3; Generalize (Rmult_lt_pos ``314`` (Rinv ``100``) H1 H3); Intro H4 | Elim PI_approx; Intros H3 _]; Assumption.
 Discriminate.
 Discriminate.
 Save.
@@ -346,7 +346,7 @@ Intros x H1 H2 H3; Elim H3; Intro H4; [ Rewrite H4; Rewrite -> sin_0; Reflexivit
 Save.
 
 Lemma PI2_RGT_0 : ``0<PI/2``.
-Cut ~(O=(2)); [Intro H; Generalize (lt_INR_0 (2) (neq_O_lt (2) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H1; Generalize (regle_signe PI (Rinv ``2``) PI_RGT_0 (Rlt_Rinv ``2`` H1)); Intro H2; Assumption | Discriminate].
+Cut ~(O=(2)); [Intro H; Generalize (lt_INR_0 (2) (neq_O_lt (2) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H1; Generalize (Rmult_lt_pos PI (Rinv ``2``) PI_RGT_0 (Rlt_Rinv ``2`` H1)); Intro H2; Assumption | Discriminate].
 Save. 
 
 Lemma Rgt_2_0 : ``0<2``.
@@ -386,7 +386,7 @@ Left; Replace ``2*PI`` with ``PI/2+3*(PI/2)``.
 Apply Rlt_compatibility; Assumption.
 Field; DiscrR.
 Apply ge0_plus_ge0_is_ge0.
-Left; Unfold Rdiv; Apply regle_signe.
+Left; Unfold Rdiv; Apply Rmult_lt_pos.
 Apply PI_RGT_0.
 Apply Rlt_Rinv; Apply Rgt_2_0. 
 Assumption.
@@ -450,7 +450,7 @@ Replace ``-2+3*/2`` with ``-(1*/2)``.
 Apply Rlt_trans with ``0``.
 Rewrite <- Ropp_O.
 Apply Rlt_Ropp.
-Apply regle_signe; [Apply Rlt_R0_R1 | Apply Rlt_Rinv; Apply Rgt_2_0].
+Apply Rmult_lt_pos; [Apply Rlt_R0_R1 | Apply Rlt_Rinv; Apply Rgt_2_0].
 Apply Rlt_R0_R1.
 Field; DiscrR.
 Simpl; Ring.
@@ -532,11 +532,11 @@ Save.
 
 (**********)
 Lemma PI4_RGT_0 : ``0<PI/4``.
-Cut ~(O=(4)); [Intro H; Generalize (lt_INR_0 (4) (neq_O_lt (4) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H1; Generalize (regle_signe PI (Rinv ``4``) PI_RGT_0 (Rlt_Rinv ``4`` H1)); Intro H2; Assumption | Discriminate].
+Cut ~(O=(4)); [Intro H; Generalize (lt_INR_0 (4) (neq_O_lt (4) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H1; Generalize (Rmult_lt_pos PI (Rinv ``4``) PI_RGT_0 (Rlt_Rinv ``4`` H1)); Intro H2; Assumption | Discriminate].
 Save.
 
 Lemma PI6_RGT_0 : ``0<PI/6``.
-Cut ~(O=(6)); [Intro H; Generalize (lt_INR_0 (6) (neq_O_lt (6) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H1; Generalize (regle_signe PI (Rinv ``6``) PI_RGT_0 (Rlt_Rinv ``6`` H1)); Intro H2; Assumption | Discriminate].
+Cut ~(O=(6)); [Intro H; Generalize (lt_INR_0 (6) (neq_O_lt (6) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H1; Generalize (Rmult_lt_pos PI (Rinv ``6``) PI_RGT_0 (Rlt_Rinv ``6`` H1)); Intro H2; Assumption | Discriminate].
 Save.
 
 Lemma _PI2_RLT_0 : ``-(PI/2)<0``.
@@ -630,14 +630,14 @@ Intros x H1 H2; Rewrite <- Ropp_O; Rewrite <- (Ropp_Ropp (cos x)); Apply Rlt_Rop
 Save.
 
 Lemma tan_gt_0 : (x:R) ``0<x`` -> ``x<PI/2`` -> ``0<(tan x)``.
-Intros x H1 H2; Unfold tan; Generalize _PI2_RLT_0; Generalize (Rlt_trans R0 x ``PI/2`` H1 H2); Intros; Generalize (Rlt_trans ``-(PI/2)`` R0 x H0 H1); Intro H5; Generalize (Rlt_trans x ``PI/2`` PI H2 PI2_Rlt_PI); Intro H7; Unfold Rdiv;  Apply regle_signe.
+Intros x H1 H2; Unfold tan; Generalize _PI2_RLT_0; Generalize (Rlt_trans R0 x ``PI/2`` H1 H2); Intros; Generalize (Rlt_trans ``-(PI/2)`` R0 x H0 H1); Intro H5; Generalize (Rlt_trans x ``PI/2`` PI H2 PI2_Rlt_PI); Intro H7; Unfold Rdiv;  Apply Rmult_lt_pos.
 Apply sin_gt_0; Assumption.
 Apply Rlt_Rinv; Apply cos_gt_0; Assumption.
 Save.
 
 Lemma tan_lt_0 : (x:R) ``-(PI/2)<x``->``x<0``->``(tan x)<0``.
 Intros x H1 H2; Unfold tan; Generalize (cos_gt_0 x H1 (Rlt_trans x ``0`` ``PI/2`` H2 PI2_RGT_0)); Intro H3; Rewrite <- Ropp_O; Replace ``(sin x)/(cos x)`` with ``- ((-(sin x))/(cos x))``.
-Rewrite <- sin_neg; Apply Rgt_Ropp; Change ``0<(sin (-x))/(cos x)``; Unfold Rdiv; Apply regle_signe.
+Rewrite <- sin_neg; Apply Rgt_Ropp; Change ``0<(sin (-x))/(cos x)``; Unfold Rdiv; Apply Rmult_lt_pos.
 Apply sin_gt_0.
 Rewrite <- Ropp_O; Apply Rgt_Ropp; Assumption.
 Apply Rlt_trans with ``PI/2``.
@@ -668,11 +668,11 @@ Intros p q; Pattern 1 p; Replace ``p`` with ``(p-q)/2+(p+q)/2``; [Pattern 3 q; R
 Save.
 
 Lemma sin_increasing_0 : (x,y:R) ``-(PI/2)<=x``->``x<=PI/2``->``-(PI/2)<=y``->``y<=PI/2``->``(sin x)<(sin y)``->``x<y``.
-Intros; Cut ``(sin ((x-y)/2))<0``; [Intro H4; Case (total_order ``(x-y)/2`` ``0``); Intro H5; [Generalize (Rlt_monotony ``2`` ``(x-y)/2`` ``0`` Rgt_2_0 H5); Replace ``2*(x-y)/2`` with ``x-y``; [Replace ``2*0`` with ``0``; [Clear H5; Intro H5; Apply Rminus_lt; Assumption | Ring] | Field; DiscrR] | Elim H5; Intro H6; [Rewrite H6 in H4; Rewrite sin_0 in H4; Elim (Rlt_antirefl ``0`` H4) | Change ``0<(x-y)/2`` in H6; Generalize (Rle_Ropp ``-(PI/2)`` y H1); Replace ``- (-(PI/2))`` with ``PI/2``; [Intro H7; Generalize (Rle_sym2 ``-y`` ``PI/2`` H7); Clear H7; Intro H7; Generalize (Rplus_le x ``PI/2`` ``-y`` ``PI/2`` H0 H7); Replace ``x+(-y)`` with ``x-y``; [Replace ``PI/2+PI/2`` with ``PI``; [Intro H8; Generalize (Rle_monotony ``(Rinv 2)`` ``x-y`` PI (Rlt_le ``0`` ``/2`` (Rlt_Rinv ``2`` Rgt_2_0)) H8); Replace ``/2*(x-y)`` with ``(x-y)/2``; [Replace ``/2*PI`` with ``PI/2``; [Intro H9; Generalize (sin_gt_0 ``(x-y)/2`` H6 (Rle_lt_trans ``(x-y)/2`` ``PI/2`` PI H9 PI2_Rlt_PI)); Intro H10; Elim (Rlt_antirefl ``(sin ((x-y)/2))`` (Rlt_trans ``(sin ((x-y)/2))`` ``0`` ``(sin ((x-y)/2))`` H4 H10)) | Field; DiscrR] | Field; DiscrR] | Field; DiscrR] | Ring] | Ring]]] | Generalize (Rlt_minus (sin x) (sin y) H3); Clear H3; Intro H3; Rewrite form4 in H3; Generalize (Rplus_le x ``PI/2`` y ``PI/2`` H0 H2); Replace ``PI/2+PI/2`` with ``PI``; [Intro H4; Generalize (Rle_monotony ``(Rinv 2)`` ``x+y`` PI (Rlt_le ``0`` ``/2`` (Rlt_Rinv ``2`` Rgt_2_0)) H4); Replace ``/2*(x+y)`` with ``(x+y)/2``; [Replace ``/2*PI`` with ``PI/2``; [Clear H4; Intro H4; Generalize (Rplus_le ``-(PI/2)`` x ``-(PI/2)`` y H H1); Replace ``-(PI/2)+(-(PI/2))`` with ``-PI``; [Intro H5; Generalize (Rle_monotony ``(Rinv 2)`` ``-PI`` ``x+y`` (Rlt_le ``0`` ``/2`` (Rlt_Rinv ``2`` Rgt_2_0)) H5); Replace ``/2*(x+y)`` with ``(x+y)/2``; [Replace ``/2*(-PI)`` with ``-(PI/2)``; [Clear H5; Intro H5; Elim H4; Intro H40; [Elim H5; Intro H50; [Generalize (cos_gt_0 ``(x+y)/2`` H50 H40); Intro H6; Generalize (Rlt_monotony ``2`` ``0`` ``(cos ((x+y)/2))`` Rgt_2_0 H6); Replace ``2*0`` with ``0``; [Clear H6; Intro H6; Case (case_Rabsolu ``(sin ((x-y)/2))``); Intro H7; [Assumption | Generalize (Rle_sym2 ``0`` ``(sin ((x-y)/2))`` H7); Clear H7; Intro H7; Generalize (regle_signe_le ``2*(cos ((x+y)/2))`` ``(sin ((x-y)/2))`` (Rlt_le ``0`` ``2*(cos ((x+y)/2))`` H6) H7); Intro H8; Generalize (Rle_lt_trans ``0`` ``2*(cos ((x+y)/2))*(sin ((x-y)/2))`` ``0`` H8 H3); Intro H9; Elim (Rlt_antirefl ``0`` H9)] | Ring] | Rewrite <- H50 in H3; Rewrite cos_neg in H3; Rewrite cos_PI2 in H3; Rewrite Rmult_Or in H3; Rewrite Rmult_Ol in H3; Elim (Rlt_antirefl ``0`` H3)] | Rewrite H40 in H3; Rewrite cos_PI2 in H3; Rewrite Rmult_Or in H3; Rewrite Rmult_Ol in H3; Elim (Rlt_antirefl ``0`` H3)] | Field; DiscrR] | Field; DiscrR] | Field; DiscrR] | Field; DiscrR] | Field; DiscrR] | Field; DiscrR]].
+Intros; Cut ``(sin ((x-y)/2))<0``; [Intro H4; Case (total_order ``(x-y)/2`` ``0``); Intro H5; [Generalize (Rlt_monotony ``2`` ``(x-y)/2`` ``0`` Rgt_2_0 H5); Replace ``2*(x-y)/2`` with ``x-y``; [Replace ``2*0`` with ``0``; [Clear H5; Intro H5; Apply Rminus_lt; Assumption | Ring] | Field; DiscrR] | Elim H5; Intro H6; [Rewrite H6 in H4; Rewrite sin_0 in H4; Elim (Rlt_antirefl ``0`` H4) | Change ``0<(x-y)/2`` in H6; Generalize (Rle_Ropp ``-(PI/2)`` y H1); Replace ``- (-(PI/2))`` with ``PI/2``; [Intro H7; Generalize (Rle_sym2 ``-y`` ``PI/2`` H7); Clear H7; Intro H7; Generalize (Rplus_le x ``PI/2`` ``-y`` ``PI/2`` H0 H7); Replace ``x+(-y)`` with ``x-y``; [Replace ``PI/2+PI/2`` with ``PI``; [Intro H8; Generalize (Rle_monotony ``(Rinv 2)`` ``x-y`` PI (Rlt_le ``0`` ``/2`` (Rlt_Rinv ``2`` Rgt_2_0)) H8); Replace ``/2*(x-y)`` with ``(x-y)/2``; [Replace ``/2*PI`` with ``PI/2``; [Intro H9; Generalize (sin_gt_0 ``(x-y)/2`` H6 (Rle_lt_trans ``(x-y)/2`` ``PI/2`` PI H9 PI2_Rlt_PI)); Intro H10; Elim (Rlt_antirefl ``(sin ((x-y)/2))`` (Rlt_trans ``(sin ((x-y)/2))`` ``0`` ``(sin ((x-y)/2))`` H4 H10)) | Field; DiscrR] | Field; DiscrR] | Field; DiscrR] | Ring] | Ring]]] | Generalize (Rlt_minus (sin x) (sin y) H3); Clear H3; Intro H3; Rewrite form4 in H3; Generalize (Rplus_le x ``PI/2`` y ``PI/2`` H0 H2); Replace ``PI/2+PI/2`` with ``PI``; [Intro H4; Generalize (Rle_monotony ``(Rinv 2)`` ``x+y`` PI (Rlt_le ``0`` ``/2`` (Rlt_Rinv ``2`` Rgt_2_0)) H4); Replace ``/2*(x+y)`` with ``(x+y)/2``; [Replace ``/2*PI`` with ``PI/2``; [Clear H4; Intro H4; Generalize (Rplus_le ``-(PI/2)`` x ``-(PI/2)`` y H H1); Replace ``-(PI/2)+(-(PI/2))`` with ``-PI``; [Intro H5; Generalize (Rle_monotony ``(Rinv 2)`` ``-PI`` ``x+y`` (Rlt_le ``0`` ``/2`` (Rlt_Rinv ``2`` Rgt_2_0)) H5); Replace ``/2*(x+y)`` with ``(x+y)/2``; [Replace ``/2*(-PI)`` with ``-(PI/2)``; [Clear H5; Intro H5; Elim H4; Intro H40; [Elim H5; Intro H50; [Generalize (cos_gt_0 ``(x+y)/2`` H50 H40); Intro H6; Generalize (Rlt_monotony ``2`` ``0`` ``(cos ((x+y)/2))`` Rgt_2_0 H6); Replace ``2*0`` with ``0``; [Clear H6; Intro H6; Case (case_Rabsolu ``(sin ((x-y)/2))``); Intro H7; [Assumption | Generalize (Rle_sym2 ``0`` ``(sin ((x-y)/2))`` H7); Clear H7; Intro H7; Generalize (Rmult_lt_pos_le ``2*(cos ((x+y)/2))`` ``(sin ((x-y)/2))`` (Rlt_le ``0`` ``2*(cos ((x+y)/2))`` H6) H7); Intro H8; Generalize (Rle_lt_trans ``0`` ``2*(cos ((x+y)/2))*(sin ((x-y)/2))`` ``0`` H8 H3); Intro H9; Elim (Rlt_antirefl ``0`` H9)] | Ring] | Rewrite <- H50 in H3; Rewrite cos_neg in H3; Rewrite cos_PI2 in H3; Rewrite Rmult_Or in H3; Rewrite Rmult_Ol in H3; Elim (Rlt_antirefl ``0`` H3)] | Rewrite H40 in H3; Rewrite cos_PI2 in H3; Rewrite Rmult_Or in H3; Rewrite Rmult_Ol in H3; Elim (Rlt_antirefl ``0`` H3)] | Field; DiscrR] | Field; DiscrR] | Field; DiscrR] | Field; DiscrR] | Field; DiscrR] | Field; DiscrR]].
 Save.
 
 Lemma sin_increasing_1 : (x,y:R) ``-(PI/2)<=x``->``x<=PI/2``->``-(PI/2)<=y``->``y<=PI/2``->``x<y``->``(sin x)<(sin y)``.
-Intros; Generalize (Rlt_compatibility ``x`` ``x`` ``y`` H3); Intro H4; Generalize (Rplus_le ``-(PI/2)`` x ``-(PI/2)`` x H H); Replace ``-(PI/2)+ (-(PI/2))`` with ``-PI``; [Intro H5; Generalize (Rle_lt_trans ``-PI`` ``x+x`` ``x+y`` H5 H4); Intro H6; Generalize (Rlt_monotony ``(Rinv 2)`` ``-PI`` ``x+y`` (Rlt_Rinv ``2`` Rgt_2_0) H6); Replace ``/2*(-PI)`` with ``-(PI/2)``; [Replace ``/2*(x+y)`` with ``(x+y)/2``; [Clear H4 H5 H6; Intro H4; Generalize (Rlt_compatibility ``y`` ``x`` ``y`` H3); Intro H5; Rewrite Rplus_sym in H5; Generalize (Rplus_le y ``PI/2`` y ``PI/2`` H2 H2); Replace ``PI/2+ PI/2`` with ``PI``; [Intro H6; Generalize (Rlt_le_trans ``x+y`` ``y+y`` PI H5 H6); Intro H7; Generalize (Rlt_monotony ``(Rinv 2)``  ``x+y`` PI (Rlt_Rinv ``2`` Rgt_2_0) H7); Replace ``/2*PI`` with ``PI/2``; [Replace ``/2*(x+y)`` with ``(x+y)/2``; [Clear H5 H6 H7; Intro H5; Generalize (Rle_Ropp ``-(PI/2)`` y H1); Rewrite Ropp_Ropp; Clear H1; Intro H1; Generalize (Rle_sym2 ``-y`` ``PI/2`` H1); Clear H1; Intro H1; Generalize (Rle_Ropp y ``PI/2`` H2); Clear H2; Intro H2; Generalize (Rle_sym2 ``-(PI/2)`` ``-y`` H2); Clear H2; Intro H2; Generalize (Rlt_compatibility ``-y`` x y H3); Replace ``-y+x`` with ``x-y``; [Replace ``-y+y`` with ``0``; [Intro H6; Generalize (Rlt_monotony ``(Rinv 2)``  ``x-y`` ``0`` (Rlt_Rinv ``2`` Rgt_2_0) H6); Rewrite Rmult_Or; Replace ``/2*(x-y)`` with ``(x-y)/2``; [Clear H6; Intro H6; Generalize (Rplus_le  ``-(PI/2)`` x ``-(PI/2)`` ``-y`` H H2); Replace ``-(PI/2)+ (-(PI/2))`` with ``-PI``; [Replace `` x+ -y`` with ``x-y``; [Intro H7; Generalize (Rle_monotony ``(Rinv 2)`` ``-PI`` ``x-y`` (Rlt_le ``0`` ``/2`` (Rlt_Rinv ``2`` Rgt_2_0)) H7); Replace ``/2*(-PI)`` with ``-(PI/2)``; [Replace ``/2*(x-y)`` with ``(x-y)/2``; [Clear H7; Intro H7; Clear H H0 H1 H2; Apply Rminus_lt; Rewrite form4; Generalize (cos_gt_0 ``(x+y)/2`` H4 H5); Intro H8; Generalize (regle_signe ``2`` ``(cos ((x+y)/2))`` Rgt_2_0 H8); Clear H8; Intro H8; Cut ``-PI< -(PI/2)``; [Intro H9; Generalize (sin_lt_0_var ``(x-y)/2`` (Rlt_le_trans ``-PI`` ``-(PI/2)`` ``(x-y)/2`` H9 H7) H6); Intro H10; Generalize (Rlt_anti_monotony ``(sin ((x-y)/2))`` ``0`` ``2*(cos ((x+y)/2))`` H10 H8); Intro H11; Rewrite Rmult_Or in H11; Rewrite Rmult_sym; Assumption | Apply Rlt_Ropp; Apply PI2_Rlt_PI] | Field] | Field] | Ring] | Field] | Field] | Ring] | Ring] | Field] | Field] | Field] | Field] | Field] | Field]; DiscrR.
+Intros; Generalize (Rlt_compatibility ``x`` ``x`` ``y`` H3); Intro H4; Generalize (Rplus_le ``-(PI/2)`` x ``-(PI/2)`` x H H); Replace ``-(PI/2)+ (-(PI/2))`` with ``-PI``; [Intro H5; Generalize (Rle_lt_trans ``-PI`` ``x+x`` ``x+y`` H5 H4); Intro H6; Generalize (Rlt_monotony ``(Rinv 2)`` ``-PI`` ``x+y`` (Rlt_Rinv ``2`` Rgt_2_0) H6); Replace ``/2*(-PI)`` with ``-(PI/2)``; [Replace ``/2*(x+y)`` with ``(x+y)/2``; [Clear H4 H5 H6; Intro H4; Generalize (Rlt_compatibility ``y`` ``x`` ``y`` H3); Intro H5; Rewrite Rplus_sym in H5; Generalize (Rplus_le y ``PI/2`` y ``PI/2`` H2 H2); Replace ``PI/2+ PI/2`` with ``PI``; [Intro H6; Generalize (Rlt_le_trans ``x+y`` ``y+y`` PI H5 H6); Intro H7; Generalize (Rlt_monotony ``(Rinv 2)``  ``x+y`` PI (Rlt_Rinv ``2`` Rgt_2_0) H7); Replace ``/2*PI`` with ``PI/2``; [Replace ``/2*(x+y)`` with ``(x+y)/2``; [Clear H5 H6 H7; Intro H5; Generalize (Rle_Ropp ``-(PI/2)`` y H1); Rewrite Ropp_Ropp; Clear H1; Intro H1; Generalize (Rle_sym2 ``-y`` ``PI/2`` H1); Clear H1; Intro H1; Generalize (Rle_Ropp y ``PI/2`` H2); Clear H2; Intro H2; Generalize (Rle_sym2 ``-(PI/2)`` ``-y`` H2); Clear H2; Intro H2; Generalize (Rlt_compatibility ``-y`` x y H3); Replace ``-y+x`` with ``x-y``; [Replace ``-y+y`` with ``0``; [Intro H6; Generalize (Rlt_monotony ``(Rinv 2)``  ``x-y`` ``0`` (Rlt_Rinv ``2`` Rgt_2_0) H6); Rewrite Rmult_Or; Replace ``/2*(x-y)`` with ``(x-y)/2``; [Clear H6; Intro H6; Generalize (Rplus_le  ``-(PI/2)`` x ``-(PI/2)`` ``-y`` H H2); Replace ``-(PI/2)+ (-(PI/2))`` with ``-PI``; [Replace `` x+ -y`` with ``x-y``; [Intro H7; Generalize (Rle_monotony ``(Rinv 2)`` ``-PI`` ``x-y`` (Rlt_le ``0`` ``/2`` (Rlt_Rinv ``2`` Rgt_2_0)) H7); Replace ``/2*(-PI)`` with ``-(PI/2)``; [Replace ``/2*(x-y)`` with ``(x-y)/2``; [Clear H7; Intro H7; Clear H H0 H1 H2; Apply Rminus_lt; Rewrite form4; Generalize (cos_gt_0 ``(x+y)/2`` H4 H5); Intro H8; Generalize (Rmult_lt_pos ``2`` ``(cos ((x+y)/2))`` Rgt_2_0 H8); Clear H8; Intro H8; Cut ``-PI< -(PI/2)``; [Intro H9; Generalize (sin_lt_0_var ``(x-y)/2`` (Rlt_le_trans ``-PI`` ``-(PI/2)`` ``(x-y)/2`` H9 H7) H6); Intro H10; Generalize (Rlt_anti_monotony ``(sin ((x-y)/2))`` ``0`` ``2*(cos ((x+y)/2))`` H10 H8); Intro H11; Rewrite Rmult_Or in H11; Rewrite Rmult_sym; Assumption | Apply Rlt_Ropp; Apply PI2_Rlt_PI] | Field] | Field] | Ring] | Field] | Field] | Ring] | Ring] | Field] | Field] | Field] | Field] | Field] | Field]; DiscrR.
 Save.
 
 Lemma sin_decreasing_0 : (x,y:R) ``x<=3*(PI/2)``-> ``PI/2<=x`` -> ``y<=3*(PI/2)``-> ``PI/2<=y`` -> ``(sin x)<(sin y)`` -> ``y<x``.
@@ -710,11 +710,11 @@ Intros; Unfold tan;Rewrite sin_minus; Field; Repeat Apply prod_neq_R0; Assumptio
 Save.
 
 Lemma tan_increasing_0 : (x,y:R) ``-(PI/4)<=x``->``x<=PI/4`` ->``-(PI/4)<=y``->``y<=PI/4``->``(tan x)<(tan y)``->``x<y``.
-Intros; Generalize PI4_RLT_PI2; Intro H4; Generalize (Rlt_Ropp ``PI/4`` ``PI/2`` H4); Intro H5; Change ``-(PI/2)< -(PI/4)`` in H5; Generalize (cos_gt_0 x (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` x H5 H) (Rle_lt_trans x ``PI/4`` ``PI/2`` H0 H4)); Intro HP1; Generalize (cos_gt_0 y (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` y H5 H1) (Rle_lt_trans y ``PI/4`` ``PI/2`` H2 H4)); Intro HP2; Generalize (not_sym ``0`` (cos x) (Rlt_not_eq ``0`` (cos x) (cos_gt_0 x (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` x H5 H) (Rle_lt_trans x ``PI/4`` ``PI/2`` H0 H4)))); Intro H6; Generalize (not_sym ``0`` (cos y) (Rlt_not_eq ``0`` (cos y) (cos_gt_0 y (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` y H5 H1) (Rle_lt_trans y ``PI/4`` ``PI/2`` H2 H4)))); Intro H7; Generalize (tan_diff x y H6 H7); Intro H8; Generalize (Rlt_minus (tan x) (tan y) H3); Clear H3; Intro H3; Rewrite H8 in H3; Cut ``(sin (x-y))<0``; [  Intro H9; Generalize (Rle_Ropp ``-(PI/4)`` y H1); Rewrite Ropp_Ropp; Intro H10; Generalize (Rle_sym2 ``-y`` ``PI/4`` H10); Clear H10; Intro H10; Generalize (Rle_Ropp y ``PI/4`` H2); Intro H11; Generalize (Rle_sym2 ``-(PI/4)`` ``-y`` H11); Clear H11; Intro H11; Generalize (Rplus_le ``-(PI/4)`` x ``-(PI/4)`` ``-y`` H H11); Generalize (Rplus_le x ``PI/4`` ``-y`` ``PI/4`` H0 H10); Replace ``x+ -y`` with ``x-y``; [Replace ``PI/4+PI/4`` with ``PI/2``; [Replace ``-(PI/4)+ -(PI/4)`` with ``-(PI/2)``; [Intros; Case (total_order ``0`` ``x-y``); Intro H14; [Generalize (sin_gt_0 ``x-y`` H14 (Rle_lt_trans ``x-y`` ``PI/2`` PI H12 PI2_Rlt_PI)); Intro H15; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` ``(sin (x-y))`` ``0`` H15 H9)) | Elim H14; Intro H15; [Rewrite <- H15 in H9; Rewrite -> sin_0 in H9;  Elim (Rlt_antirefl ``0`` H9) | Apply Rminus_lt; Assumption]] | Field; DiscrR] | Field; DiscrR] | Ring]   |   Case (case_Rabsolu ``(sin (x-y))``); Intro H9; [Assumption | Generalize (Rle_sym2 ``0`` ``(sin (x-y))`` H9); Clear H9; Intro H9; Generalize (Rlt_Rinv (cos x) HP1); Intro H10; Generalize (Rlt_Rinv (cos y) HP2); Intro H11; Generalize (regle_signe (Rinv (cos x)) (Rinv (cos y)) H10 H11); Replace ``/(cos x)*/(cos y)`` with ``/((cos x)*(cos y))``; [Intro H12; Generalize (regle_signe_le ``(sin (x-y))`` ``/((cos x)*(cos y))`` H9 (Rlt_le ``0`` ``/((cos x)*(cos y))`` H12)); Intro H13; Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` ``(sin (x-y))*/((cos x)*(cos y))`` ``0`` H13 H3)) | Field; Repeat Apply prod_neq_R0; Assumption]]  ].
+Intros; Generalize PI4_RLT_PI2; Intro H4; Generalize (Rlt_Ropp ``PI/4`` ``PI/2`` H4); Intro H5; Change ``-(PI/2)< -(PI/4)`` in H5; Generalize (cos_gt_0 x (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` x H5 H) (Rle_lt_trans x ``PI/4`` ``PI/2`` H0 H4)); Intro HP1; Generalize (cos_gt_0 y (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` y H5 H1) (Rle_lt_trans y ``PI/4`` ``PI/2`` H2 H4)); Intro HP2; Generalize (not_sym ``0`` (cos x) (Rlt_not_eq ``0`` (cos x) (cos_gt_0 x (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` x H5 H) (Rle_lt_trans x ``PI/4`` ``PI/2`` H0 H4)))); Intro H6; Generalize (not_sym ``0`` (cos y) (Rlt_not_eq ``0`` (cos y) (cos_gt_0 y (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` y H5 H1) (Rle_lt_trans y ``PI/4`` ``PI/2`` H2 H4)))); Intro H7; Generalize (tan_diff x y H6 H7); Intro H8; Generalize (Rlt_minus (tan x) (tan y) H3); Clear H3; Intro H3; Rewrite H8 in H3; Cut ``(sin (x-y))<0``; [  Intro H9; Generalize (Rle_Ropp ``-(PI/4)`` y H1); Rewrite Ropp_Ropp; Intro H10; Generalize (Rle_sym2 ``-y`` ``PI/4`` H10); Clear H10; Intro H10; Generalize (Rle_Ropp y ``PI/4`` H2); Intro H11; Generalize (Rle_sym2 ``-(PI/4)`` ``-y`` H11); Clear H11; Intro H11; Generalize (Rplus_le ``-(PI/4)`` x ``-(PI/4)`` ``-y`` H H11); Generalize (Rplus_le x ``PI/4`` ``-y`` ``PI/4`` H0 H10); Replace ``x+ -y`` with ``x-y``; [Replace ``PI/4+PI/4`` with ``PI/2``; [Replace ``-(PI/4)+ -(PI/4)`` with ``-(PI/2)``; [Intros; Case (total_order ``0`` ``x-y``); Intro H14; [Generalize (sin_gt_0 ``x-y`` H14 (Rle_lt_trans ``x-y`` ``PI/2`` PI H12 PI2_Rlt_PI)); Intro H15; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` ``(sin (x-y))`` ``0`` H15 H9)) | Elim H14; Intro H15; [Rewrite <- H15 in H9; Rewrite -> sin_0 in H9;  Elim (Rlt_antirefl ``0`` H9) | Apply Rminus_lt; Assumption]] | Field; DiscrR] | Field; DiscrR] | Ring]   |   Case (case_Rabsolu ``(sin (x-y))``); Intro H9; [Assumption | Generalize (Rle_sym2 ``0`` ``(sin (x-y))`` H9); Clear H9; Intro H9; Generalize (Rlt_Rinv (cos x) HP1); Intro H10; Generalize (Rlt_Rinv (cos y) HP2); Intro H11; Generalize (Rmult_lt_pos (Rinv (cos x)) (Rinv (cos y)) H10 H11); Replace ``/(cos x)*/(cos y)`` with ``/((cos x)*(cos y))``; [Intro H12; Generalize (Rmult_lt_pos_le ``(sin (x-y))`` ``/((cos x)*(cos y))`` H9 (Rlt_le ``0`` ``/((cos x)*(cos y))`` H12)); Intro H13; Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` ``(sin (x-y))*/((cos x)*(cos y))`` ``0`` H13 H3)) | Field; Repeat Apply prod_neq_R0; Assumption]]  ].
 Save.
 
 Lemma tan_increasing_1 : (x,y:R) ``-(PI/4)<=x``->``x<=PI/4`` ->``-(PI/4)<=y``->``y<=PI/4``->``x<y``->``(tan x)<(tan y)``.
-Intros; Apply Rminus_lt; Generalize PI4_RLT_PI2; Intro H4; Generalize (Rlt_Ropp ``PI/4`` ``PI/2`` H4); Intro H5; Change ``-(PI/2)< -(PI/4)`` in H5; Generalize (cos_gt_0 x (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` x H5 H) (Rle_lt_trans x ``PI/4`` ``PI/2`` H0 H4)); Intro HP1; Generalize (cos_gt_0 y (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` y H5 H1) (Rle_lt_trans y ``PI/4`` ``PI/2`` H2 H4)); Intro HP2; Generalize (not_sym ``0`` (cos x) (Rlt_not_eq ``0`` (cos x) (cos_gt_0 x (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` x H5 H) (Rle_lt_trans x ``PI/4`` ``PI/2`` H0 H4)))); Intro H6; Generalize (not_sym ``0`` (cos y) (Rlt_not_eq ``0`` (cos y) (cos_gt_0 y (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` y H5 H1) (Rle_lt_trans y ``PI/4`` ``PI/2`` H2 H4)))); Intro H7; Rewrite (tan_diff x y H6 H7); Generalize (Rlt_Rinv (cos x) HP1); Intro H10; Generalize (Rlt_Rinv (cos y) HP2); Intro H11; Generalize (regle_signe (Rinv (cos x)) (Rinv (cos y)) H10 H11); Replace ``/(cos x)*/(cos y)`` with ``/((cos x)*(cos y))``; [Clear H10 H11; Intro H8; Generalize (Rle_Ropp y ``PI/4`` H2); Intro H11; Generalize (Rle_sym2 ``-(PI/4)`` ``-y`` H11); Clear H11; Intro H11; Generalize (Rplus_le ``-(PI/4)`` x ``-(PI/4)`` ``-y`` H H11); Replace ``x+ -y`` with ``x-y``; [Replace ``-(PI/4)+ -(PI/4)`` with ``-(PI/2)``; [Clear H11; Intro H9; Generalize (Rlt_minus x y H3); Clear H3; Intro H3; Clear H H0 H1 H2 H4 H5 HP1 HP2; Generalize PI2_Rlt_PI; Intro H1; Generalize (Rlt_Ropp ``PI/2`` PI H1); Clear H1; Intro H1; Generalize (sin_lt_0_var ``x-y`` (Rlt_le_trans ``-PI`` ``-(PI/2)`` ``x-y`` H1 H9) H3); Intro H2; Generalize (Rlt_anti_monotony ``(sin (x-y))`` ``0`` ``/((cos x)*(cos y))`` H2 H8); Rewrite Rmult_Or; Intro H4; Assumption | Field; DiscrR] | Ring] | Field; Repeat Apply prod_neq_R0; Assumption].
+Intros; Apply Rminus_lt; Generalize PI4_RLT_PI2; Intro H4; Generalize (Rlt_Ropp ``PI/4`` ``PI/2`` H4); Intro H5; Change ``-(PI/2)< -(PI/4)`` in H5; Generalize (cos_gt_0 x (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` x H5 H) (Rle_lt_trans x ``PI/4`` ``PI/2`` H0 H4)); Intro HP1; Generalize (cos_gt_0 y (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` y H5 H1) (Rle_lt_trans y ``PI/4`` ``PI/2`` H2 H4)); Intro HP2; Generalize (not_sym ``0`` (cos x) (Rlt_not_eq ``0`` (cos x) (cos_gt_0 x (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` x H5 H) (Rle_lt_trans x ``PI/4`` ``PI/2`` H0 H4)))); Intro H6; Generalize (not_sym ``0`` (cos y) (Rlt_not_eq ``0`` (cos y) (cos_gt_0 y (Rlt_le_trans ``-(PI/2)`` ``-(PI/4)`` y H5 H1) (Rle_lt_trans y ``PI/4`` ``PI/2`` H2 H4)))); Intro H7; Rewrite (tan_diff x y H6 H7); Generalize (Rlt_Rinv (cos x) HP1); Intro H10; Generalize (Rlt_Rinv (cos y) HP2); Intro H11; Generalize (Rmult_lt_pos (Rinv (cos x)) (Rinv (cos y)) H10 H11); Replace ``/(cos x)*/(cos y)`` with ``/((cos x)*(cos y))``; [Clear H10 H11; Intro H8; Generalize (Rle_Ropp y ``PI/4`` H2); Intro H11; Generalize (Rle_sym2 ``-(PI/4)`` ``-y`` H11); Clear H11; Intro H11; Generalize (Rplus_le ``-(PI/4)`` x ``-(PI/4)`` ``-y`` H H11); Replace ``x+ -y`` with ``x-y``; [Replace ``-(PI/4)+ -(PI/4)`` with ``-(PI/2)``; [Clear H11; Intro H9; Generalize (Rlt_minus x y H3); Clear H3; Intro H3; Clear H H0 H1 H2 H4 H5 HP1 HP2; Generalize PI2_Rlt_PI; Intro H1; Generalize (Rlt_Ropp ``PI/2`` PI H1); Clear H1; Intro H1; Generalize (sin_lt_0_var ``x-y`` (Rlt_le_trans ``-PI`` ``-(PI/2)`` ``x-y`` H1 H9) H3); Intro H2; Generalize (Rlt_anti_monotony ``(sin (x-y))`` ``0`` ``/((cos x)*(cos y))`` H2 H8); Rewrite Rmult_Or; Intro H4; Assumption | Field; DiscrR] | Ring] | Field; Repeat Apply prod_neq_R0; Assumption].
 Save.
 
 Lemma sin_incr_0 : (x,y:R) ``-(PI/2)<=x``->``x<=PI/2``->``-(PI/2)<=y``->``y<=PI/2``->``(sin x)<=(sin y)``->``x<=y``.
@@ -778,7 +778,7 @@ Rewrite cos_sin; Replace ``PI/2+PI/4`` with ``-(PI/4)+PI``; [Rewrite neg_sin; Re
 Save.
 
 Lemma cos_PI4 : ``(cos (PI/4))==1/(sqrt 2)``.
-Apply Rsqr_inj; [ Apply cos_ge_0; [Left; Apply (Rlt_trans ``-(PI/2)`` R0 ``PI/4`` _PI2_RLT_0 PI4_RGT_0) | Left; Apply PI4_RLT_PI2]  |  Left; Apply (regle_signe R1 ``(Rinv (sqrt 2))``); [ Apply Rlt_R0_R1 | Apply Rlt_Rinv]; Apply Rlt_sqrt2_0  |  Rewrite Rsqr_div; [Rewrite Rsqr_1; Rewrite Rsqr_sqrt; [Unfold Rsqr; Pattern 1 ``(cos (PI/4))``; Rewrite <- sin_cos_PI4; Replace ``(sin (PI/4))*(cos (PI/4))`` with ``(1/2)*(2*(sin (PI/4))*(cos (PI/4)))``; [ Rewrite <- sin_2a; Replace ``2*(PI/4)`` with ``PI/2``; [Rewrite sin_PI2; Field; DiscrR | Field; DiscrR] | Field; DiscrR] | Left; Apply Rgt_2_0] | Apply sqrt2_neq_0]].
+Apply Rsqr_inj; [ Apply cos_ge_0; [Left; Apply (Rlt_trans ``-(PI/2)`` R0 ``PI/4`` _PI2_RLT_0 PI4_RGT_0) | Left; Apply PI4_RLT_PI2]  |  Left; Apply (Rmult_lt_pos R1 ``(Rinv (sqrt 2))``); [ Apply Rlt_R0_R1 | Apply Rlt_Rinv]; Apply Rlt_sqrt2_0  |  Rewrite Rsqr_div; [Rewrite Rsqr_1; Rewrite Rsqr_sqrt; [Unfold Rsqr; Pattern 1 ``(cos (PI/4))``; Rewrite <- sin_cos_PI4; Replace ``(sin (PI/4))*(cos (PI/4))`` with ``(1/2)*(2*(sin (PI/4))*(cos (PI/4)))``; [ Rewrite <- sin_2a; Replace ``2*(PI/4)`` with ``PI/2``; [Rewrite sin_PI2; Field; DiscrR | Field; DiscrR] | Field; DiscrR] | Left; Apply Rgt_2_0] | Apply sqrt2_neq_0]].
 Save.
 
 Lemma sin_PI4 : ``(sin (PI/4))==1/(sqrt 2)``.
@@ -810,7 +810,7 @@ Apply r_Rmult_mult with ``2*(cos (PI/6))``; [Replace ``2*(cos (PI/6))*(sin (PI/6
 Save.
 
 Lemma cos_PI6 : ``(cos (PI/6))==(sqrt 3)/2``.
-Apply Rsqr_inj; [ Apply cos_ge_0; [Left; Apply (Rlt_trans ``-(PI/2)`` R0 ``PI/6`` _PI2_RLT_0 PI6_RGT_0) | Left; Apply PI6_RLT_PI2]  |  Left; Apply (regle_signe ``(sqrt 3)`` ``(Rinv 2)``); [Apply Rlt_sqrt3_0 | Apply Rlt_Rinv; Apply Rgt_2_0]  |  Rewrite Rsqr_div; [Rewrite cos2; Unfold Rsqr; Rewrite sin_PI6; Rewrite sqrt_def; [ Field; DiscrR | Left; Apply Rgt_3_0] | DiscrR]].
+Apply Rsqr_inj; [ Apply cos_ge_0; [Left; Apply (Rlt_trans ``-(PI/2)`` R0 ``PI/6`` _PI2_RLT_0 PI6_RGT_0) | Left; Apply PI6_RLT_PI2]  |  Left; Apply (Rmult_lt_pos ``(sqrt 3)`` ``(Rinv 2)``); [Apply Rlt_sqrt3_0 | Apply Rlt_Rinv; Apply Rgt_2_0]  |  Rewrite Rsqr_div; [Rewrite cos2; Unfold Rsqr; Rewrite sin_PI6; Rewrite sqrt_def; [ Field; DiscrR | Left; Apply Rgt_3_0] | DiscrR]].
 Save.
 
 Lemma tan_PI6 : ``(tan (PI/6))==1/(sqrt 3)``.