proposition: Lemma cos_pos : forall x, open_interval (- PI/2) (PI/2) x -> 0 < cos x.
proof: Proof. intros x [xlb xub] ; apply cos_gt_0 ; unfold Rdiv ; ring_simplify ; assumption. 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