proposition: Lemma cos_derivable : derivable cos.
proof: Proof. eapply derivable_ext. intro x ; symmetry ; apply cos_cosine. apply derivable_cosine. 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