proposition: Lemma sin_decr_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; case (Rtotal_order x y); intro H4; [ left; apply (sin_decreasing_1 x y H H0 H1 H2 H4) | elim H4; intro H5; [ case (Rtotal_order (sin x) (sin y)); intro H6; [ generalize (sin_decreasing_0 x y H H0 H1 H2 H6); intro H8; rewrite H5 in H8; elim (Rlt_irrefl y H8) | elim H6; intro H7; [ right; symmetry in |- *; assumption | left; assumption ] ] | elim (Rlt_irrefl x (Rle_lt_trans x y x H3 H5)) ] ]. 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