proposition: Lemma polyseq_poly n E : E n.-1 != 0 -> \poly_(i < n) E i = mkseq [eta E] n :> seq R.
proof: Proof. rewrite unlock; case: n => [|n] nzEn; first by rewrite polyseqC eqxx. by rewrite (@PolyK 0) // -nth_last nth_mkseq size_mkseq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)