proposition: Lemma tan_increasing_0 : forall x y:R, - (PI / 4) <= x -> x <= PI / 4 -> - (PI / 4) <= y -> y <= PI / 4 -> tan x < tan y -> x < y.
proof: Proof. intros; generalize PI4_RLT_PI2; intro H4; generalize (Ropp_lt_gt_contravar (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_eq_sym (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_eq_sym (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 (Ropp_le_ge_contravar (- (PI / 4)) y H1); rewrite Ropp_involutive; intro H10; generalize (Rge_le (PI / 4) (- y) H10); clear H10; intro H10; generalize (Ropp_le_ge_contravar y (PI / 4) H2); intro H11; generalize (Rge_le (- y) (- (PI / 4)) H11); clear H11; intro H11; generalize (Rplus_le_compat (- (PI / 4)) x (- (PI / 4)) (- y) H H11); generalize (Rplus_le_compat x (PI / 4) (- y) (PI / 4) H0 H10). replace (PI / 4 + PI / 4) with (PI / 2) by field. replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)) by field. intros; case (Rtotal_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_irrefl 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_irrefl 0 H9). * apply Rminus_lt; assumption. - case (Rcase_abs (sin (x - y))); intro H9. + assumption. + generalize (Rge_le (sin (x - y)) 0 H9); clear H9; intro H9; generalize (Rinv_0_lt_compat (cos x) HP1); intro H10; generalize (Rinv_0_lt_compat (cos y) HP2); intro H11; generalize (Rmult_lt_0_compat (/ cos x) (/ 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_irrefl 0 (Rle_lt_trans 0 (sin (x - y) * / (cos x * cos y)) 0 H13 H3)). * apply Rinv_mult. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Rtrigo_def Rtrigo_alt Cos_rel Cos_plus ZArith_base Zcomplements Lia Lra Ranalysis1 Rsqrt_def PSeries_reg