proposition: Lemma derivnMXaddC n p c : (p * 'X + c%:P)^`(n.+1) = p^`(n) *+ n.+1 + p^`(n.+1) * 'X.
proof: Proof. elim: n => [|n IHn]; first by rewrite derivn1 derivMXaddC. rewrite derivnS IHn derivD derivM derivX mulr1 derivMn -!derivnS. by rewrite addrA addrAC -mulrSr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)