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