proposition: Lemma derive_pt_cos : forall x pr, derive_pt cos x pr = - sin x.
proof: Proof. intros x pr ; transitivity (- sine x). rewrite derive_pt_ext with (prg := derivable_cosine x). apply derive_pt_cosine_sine. apply cos_cosine. apply Ropp_eq_compat ; symmetry ; apply sin_sine. 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