proposition: Lemma derivXn n : 'X^n^`() = 'X^n.-1 *+ n.
proof: Proof. case: n => [|n]; first exact: derivC. apply/polyP=> i; rewrite coef_deriv coefMn !coefXn eqSS. by case: eqP => [-> // | _]; rewrite !mul0rn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)