From 3f054c565ffed6356e3eaea15495eebf637ef126 Mon Sep 17 00:00:00 2001
From: desmettr
Date: Wed, 5 Dec 2001 09:31:33 +0000
Subject: *** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2268 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Rtrigo.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index f3d9d26efd..fa07efe982 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -668,7 +668,7 @@ 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 (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]].
+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_le_pos ``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)``.
@@ -710,7 +710,7 @@ 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 (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]]  ].
+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_le_pos ``(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)``.
-- 
cgit v1.2.3