proposition: Lemma derivable_pt_sin : forall x:R, derivable_pt sin x.
proof: Proof. unfold derivable_pt; intro. exists (cos x). apply derivable_pt_lim_sin. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lra