proposition: Lemma size_Poly s : size (Poly s) <= size s.
proof: Proof. elim: s => [|c s IHs] /=; first by rewrite polyseqC eqxx. by rewrite polyseq_cons; case: ifP => // _; rewrite size_polyC; case: (~~ _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)