proposition: Lemma derive_pt_sin : forall x pr, derive_pt sin x pr = cos x.
proof: Proof. intros x pr ; transitivity (cosine x). rewrite derive_pt_ext with (prg := derivable_sine x). apply derive_pt_sine_cosine. apply sin_sine. symmetry ; apply cos_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