proposition: Lemma sin_increasing_0 : forall x y:R, - (PI / 2) <= x -> x <= PI / 2 -> - (PI / 2) <= y -> y <= PI / 2 -> sin x < sin y -> x < y.
proof: Proof. intros; cut (sin ((x - y) / 2) < 0). - intro H4; case (Rtotal_order ((x - y) / 2) 0); intro H5. { unfold Rdiv in H5;lra. } elim H5; intro H6. { rewrite H6 in H4; rewrite sin_0 in H4; elim (Rlt_irrefl 0 H4). } change (0 < (x - y) / 2) in H6; generalize (Ropp_le_ge_contravar (- (PI / 2)) y H1). rewrite Ropp_involutive. intro H7; generalize (Rge_le (PI / 2) (- y) H7); clear H7; intro H7; generalize (Rplus_le_compat x (PI / 2) (- y) (PI / 2) H0 H7). rewrite Rplus_half_diag. intro H8. assert (Hyp : 0 < 2) by lra. generalize (Rmult_le_compat_l (/ 2) (x - y) PI (Rlt_le 0 (/ 2) (Rinv_0_lt_compat 2 Hyp)) H8). repeat rewrite (Rmult_comm (/ 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_irrefl (sin ((x - y) / 2)) (Rlt_trans (sin ((x - y) / 2)) 0 (sin ((x - y) / 2)) H4 H10)). - generalize (Rlt_minus (sin x) (sin y) H3); clear H3; intro H3; rewrite form4 in H3; generalize (Rplus_le_compat x (PI / 2) y (PI / 2) H0 H2). rewrite Rplus_half_diag. assert (Hyp : 0 < 2) by prove_sup0. intro H4; generalize (Rmult_le_compat_l (/ 2) (x + y) PI (Rlt_le 0 (/ 2) (Rinv_0_lt_compat 2 Hyp)) H4). repeat rewrite (Rmult_comm (/ 2)). clear H4; intro H4; generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) y H H1); replace (- (PI / 2) + - (PI / 2)) with (- PI) by field. intro H5; generalize (Rmult_le_compat_l (/ 2) (- PI) (x + y) (Rlt_le 0 (/ 2) (Rinv_0_lt_compat 2 Hyp)) H5). replace (/ 2 * (x + y)) with ((x + y) / 2) by apply Rmult_comm. replace (/ 2 * - PI) with (- (PI / 2)) by field. clear H5; intro H5; elim H4; intro H40. 2:{ unfold Rdiv in H3. rewrite H40 in H3; assert (H50 := cos_PI2); unfold Rdiv in H50; rewrite H50 in H3; rewrite Rmult_0_r in H3; rewrite Rmult_0_l in H3; elim (Rlt_irrefl 0 H3). } elim H5; intro H50. 2:{ rewrite <- H50 in H3; rewrite cos_neg in H3; rewrite cos_PI2 in H3; rewrite Rmult_0_r in H3; rewrite Rmult_0_l in H3; elim (Rlt_irrefl 0 H3). } generalize (cos_gt_0 ((x + y) / 2) H50 H40); intro H6; generalize (Rmult_lt_compat_l 2 0 (cos ((x + y) / 2)) Hyp H6). rewrite Rmult_0_r. clear H6; intro H6; case (Rcase_abs (sin ((x - y) / 2))); intro H7. { assumption. } generalize (Rge_le (sin ((x - y) / 2)) 0 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_irrefl 0 H9). 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