proposition: Lemma nderivnMXaddC n p c : (p * 'X + c%:P)^`N(n.+1) = p^`N(n) + p^`N(n.+1) * 'X.
proof: Proof. apply/polyP=> i; rewrite coef_nderivn !coefD !coefMX coefC. rewrite !addSn /= !coef_nderivn addr0 binS mulrnDr addrC; congr (_ + _). by rewrite addSnnS; case: i; rewrite // addn0 bin_small. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)