proposition: Lemma Derive_nS f n : Derive_n f n.+1 = Derive_n (Derive f) n.
proof: Proof. elim: n => [//|n IHn]. by rewrite -[in LHS]addn1 /= -addnE addn1 IHn. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp