proposition: Lemma ex_derive_n_is_derive_n : forall f n x l, is_derive_n f n x l -> ex_derive_n f n x.
proof: Proof. intros f [|n] x l. easy. rewrite /is_derive_n /ex_derive_n => H. eexists. apply H. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp