proposition: Lemma nderivnXn m n : 'X^m^`N(n) = 'X^(m - n) *+ 'C(m, n).
proof: Proof. apply/polyP=> i; rewrite coef_nderivn coefMn !coefXn. have [lt_m_n | le_n_m] := ltnP m n. by rewrite eqn_leq leqNgt ltn_addr // mul0rn bin_small. by rewrite -{1 3}(subnKC le_n_m) eqn_add2l; 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)