proposition: Lemma size_poly1P p : reflect (exists2 c, c != 0 & p = c%:P) (size p == 1).
proof: Proof. apply: (iffP eqP) => [pC | [c nz_c ->]]; last by rewrite size_polyC nz_c. have def_p: p = (p`_0)%:P by rewrite -size1_polyC ?pC. by exists p`_0; rewrite // -polyC_eq0 -def_p -size_poly_eq0 pC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)