proposition: Lemma coefXnM n p i : ('X^n * p)`_i = if i < n then 0 else p`_(i - n).
proof: Proof. by rewrite -commr_polyXn coefMXn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)