proposition: Lemma derive_pt_cos : forall x:R, derive_pt cos x (derivable_pt_cos _) = - sin x.
proof: Proof. intros; apply derive_pt_eq_0. apply derivable_pt_lim_cos. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lra