proposition: Lemma size_poly n E : size (\poly_(i < n) E i) <= n.
proof: Proof. by rewrite unlock (leq_trans (size_Poly _)) ?size_mkseq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)