proposition: Lemma derivable_pt_exp : forall x:R, derivable_pt exp x.
proof: Proof. intro. unfold derivable_pt. exists (exp x). apply derivable_pt_lim_exp. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Ranalysis3 Exp_prop MVT Lra Lia