proposition: Lemma cos_decreasing_1 : forall x y:R, 0 <= x -> x <= PI -> 0 <= y -> y <= PI -> x < y -> cos y < cos x.
proof: Proof. intros; apply Ropp_lt_cancel; repeat rewrite <- neg_cos; rewrite (Rplus_comm x); rewrite (Rplus_comm y); generalize (Rplus_le_compat_l PI 0 x H); generalize (Rplus_le_compat_l PI x PI H0); generalize (Rplus_le_compat_l PI 0 y H1); generalize (Rplus_le_compat_l PI y PI H2); rewrite Rplus_0_r. rewrite Rplus_diag. generalize (Rplus_lt_compat_l PI x y H3); clear H H0 H1 H2 H3; intros; apply (cos_increasing_1 (PI + x) (PI + y) H3 H2 H1 H0 H). 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