proposition: Lemma is_derive_n_exp : forall n x, is_derive_n exp n x (exp x).
proof: Proof. intros [|n]. easy. simpl. induction n. apply is_derive_exp. intros x. apply is_derive_ext with exp ; cycle 1. apply is_derive_exp. simpl. intros t. apply eq_sym. now apply is_derive_unique. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis