proposition: Lemma is_derive_exp : forall x, is_derive exp x (exp x).
proof: Proof. intros x. apply is_derive_Reals. apply derivable_pt_lim_exp. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis