proposition: Lemma PI2_lower_bound : forall x, 0 < x < 2 -> 0 < cos x -> x < PI/2.
proof: Proof. intros x [xp xlt2] cx. destruct (Rtotal_order x (PI/2)) as [xltpi2 | [xeqpi2 | xgtpi2]]. - assumption. - now case (Rgt_not_eq _ _ cx); rewrite xeqpi2, cos_PI2. - destruct (MVT_cor1 cos (PI/2) x derivable_cos xgtpi2) as [c [Pc [cint1 cint2]]]. revert Pc; rewrite cos_PI2, Rminus_0_r. rewrite <- (pr_nu cos c (derivable_pt_cos c)), derive_pt_cos. assert (0 < c < 2) by (split; assert (t := PI2_RGT_0); lra). assert (0 < sin c) by now apply sin_pos_tech. intros Pc. case (Rlt_not_le _ _ cx). rewrite <- (Rplus_0_l (cos x)), Pc, Ropp_mult_distr_l_reverse. apply Rle_minus, Rmult_le_pos;[apply Rlt_le; assumption | lra ]. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia