proposition: Lemma derivMXaddC p c : (p * 'X + c%:P)^`() = p + p^`() * 'X.
proof: Proof. apply/polyP=> i; rewrite raddfD /= derivC addr0 coefD !(coefMX, coef_deriv). by case: i; rewrite ?addr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)