proposition: Lemma cos_cv_0_left : forall eps a, 0 < eps -> a < PI / 2 -> { x | open_interval a (PI / 2) x /\ cos x < eps }.
proof: Proof. intros eps a eps_pos a_ub ; destruct (sin_cv_0_right _ (PI / 2 - a) eps_pos) as [x [[x_lb x_ub] Hx]]. lra. exists (PI / 2 - x) ; rewrite cos_shift ; repeat split ; (trivial || lra). Qed.
imports: Rbase Rtactic Lra Ranalysis Ranalysis5 Rtrigo AltSeries Rfunctions Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Rextensionality Rpser_usual Rsequence_cv_facts MyRIneq Tactics