proposition: Lemma sin_decreasing_0 : forall x y:R, x <= 3 * (PI / 2) -> PI / 2 <= x -> y <= 3 * (PI / 2) -> PI / 2 <= y -> sin x < sin y -> y < x.
proof: Proof. intros; rewrite <- (sin_PI_x x) in H3; rewrite <- (sin_PI_x y) in H3; generalize (Ropp_lt_gt_contravar (sin (PI - x)) (sin (PI - y)) H3); repeat rewrite <- sin_neg; generalize (Rplus_le_compat_l (- PI) x (3 * (PI / 2)) H); generalize (Rplus_le_compat_l (- PI) (PI / 2) x H0); generalize (Rplus_le_compat_l (- PI) y (3 * (PI / 2)) H1); generalize (Rplus_le_compat_l (- PI) (PI / 2) y H2); replace (- PI + x) with (x - PI) by apply Rplus_comm. replace (- PI + PI / 2) with (- (PI / 2)) by field. replace (- PI + y) with (y - PI) by apply Rplus_comm. replace (- PI + 3 * (PI / 2)) with (PI / 2) by field. replace (- (PI - x)) with (x - PI) by ring. replace (- (PI - y)) with (y - PI) by ring. intros; change (sin (y - PI) < sin (x - PI)) in H8; apply Rplus_lt_reg_l with (- PI); rewrite Rplus_comm. rewrite (Rplus_comm _ x). apply (sin_increasing_0 (y - PI) (x - PI) H4 H5 H6 H7 H8). 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