proposition: Lemma cos_incr_1 : forall x y:R, PI <= x -> x <= 2 * PI -> PI <= y -> y <= 2 * PI -> x <= y -> cos x <= cos y.
proof: Proof. intros; case (Rtotal_order x y); intro H4; [ left; apply (cos_increasing_1 x y H H0 H1 H2 H4) | elim H4; intro H5; [ case (Rtotal_order (cos x) (cos y)); intro H6; [ left; assumption | elim H6; intro H7; [ right; assumption | generalize (cos_increasing_0 y x H1 H2 H H0 H7); intro H8; rewrite H5 in H8; elim (Rlt_irrefl y H8) ] ] | 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