proposition: Lemma coefMXn n p i : (p * 'X^n)`_i = if i < n then 0 else p`_(i - n).
proof: Proof. have [-> | /polyseqMXn->] := eqVneq p 0; last exact: nth_ncons. by rewrite mul0r !coef0 if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)