proposition: Lemma derive_pt_exp : forall x:R, derive_pt exp x (derivable_pt_exp x) = exp x.
proof: Proof. intro; apply derive_pt_eq_0. apply derivable_pt_lim_exp. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Ranalysis3 Exp_prop MVT Lra Lia