proposition: Lemma sin_decreasing_1 : forall x y:R, x <= 3 * (PI / 2) -> PI / 2 <= x -> y <= 3 * (PI / 2) -> PI / 2 <= y -> x < y -> sin y < sin x.
proof: Proof. intros; rewrite <- (sin_PI_x x); rewrite <- (sin_PI_x y); 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); generalize (Rplus_lt_compat_l (- PI) x y H3); 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 apply Rplus_comm. intros; apply Ropp_lt_cancel; repeat rewrite <- sin_neg; replace (- (PI - x)) with (x - PI) by ring. replace (- (PI - y)) with (y - PI) by ring. apply (sin_increasing_1 (x - PI) (y - PI) H7 H8 H5 H6 H4). 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