proposition: Lemma Derivation_exp x m : x \in E -> D (x ^+ m) = x ^+ m.-1 *+ m * D x.
proof: Proof. move=> Ex; case: m; first by rewrite expr0 mulr0n mul0r Derivation1. elim=> [|m IHm]; first by rewrite mul1r. rewrite exprS (Derivation_mul derD) //; last by apply: rpredX. by rewrite mulrC IHm mulrA mulrnAr -exprS -mulrDl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset prime) mathcomp(binomial ssralg poly polydiv fingroup perm) mathcomp(morphism quotient gproduct finalg zmodp cyclic) mathcomp(matrix mxalgebra mxpoly polyXY vector falgebra) mathcomp(fieldext)