proposition: Lemma derivnXn m n : 'X^m^`(n) = 'X^(m - n) *+ m ^_ n.
proof: Proof. apply/polyP=>i; rewrite coef_derivn coefMn !coefXn. case: (ltnP m n) => [lt_m_n | le_m_n]. by rewrite eqn_leq leqNgt ltn_addr // mul0rn ffact_small. by rewrite -{1 3}(subnKC le_m_n) 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)