proposition: Lemma size_poly_eq n E : E n.-1 != 0 -> size (\poly_(i < n) E i) = n.
proof: Proof. by move/polyseq_poly->; apply: size_mkseq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)