proposition: Lemma polyseqMXn n p : p != 0 -> p * 'X^n = ncons n 0 p :> seq R.
proof: Proof. case: n => [|n] nz_p; first by rewrite mulr1. elim: n => [|n IHn]; first exact: polyseqMX. by rewrite exprSr mulrA polyseqMX -?nil_poly IHn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)