proposition: Lemma coefMX p i : (p * 'X)`_i = (if (i == 0)%N then 0 else p`_i.-1).
proof: Proof. rewrite coefMr big_ord_recl coefX ?simp. case: i => [|i]; rewrite ?big_ord0 //= big_ord_recl polyseqX subn1 /=. by rewrite big1 ?simp // => j _; rewrite nth_nil !simp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)