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