proposition: Lemma poly0Vpos p : {p = 0} + {size p > 0}.
proof: Proof. by rewrite lt0n size_poly_eq0; case: eqVneq; [left | right]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)