proposition: Lemma ex_derive_nSS f n : ex_derive_n f n.+2 = ex_derive_n (Derive f) n.+1.
proof: Proof. case: n => [//|n]. by rewrite /ex_derive_n Derive_nS. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp