proposition: Lemma cos_decreasing_0 : forall x y:R, 0 <= x -> x <= PI -> 0 <= y -> y <= PI -> cos x < cos y -> y < x.
proof: Proof. intros; generalize (Ropp_lt_gt_contravar (cos x) (cos y) H3); repeat rewrite <- neg_cos; intro H4; change (cos (y + PI) < cos (x + PI)) in H4; rewrite (Rplus_comm x) in H4; rewrite (Rplus_comm y) in H4; 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. clear H H0 H1 H2 H3; intros; apply Rplus_lt_reg_l with PI; apply (cos_increasing_0 (PI + y) (PI + x) H0 H H2 H1 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