proposition: Lemma is_derive_n_exp : forall n x, is_derive_n exp n x (exp x).
proof: Proof. help_is_derive_n_whole n x. - by auto_derive; last by rewrite Rmult_1_l. - by auto_derive; last by rewrite Rmult_1_l. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp