proposition: Lemma msize_poly1P p : reflect (exists2 c, c != 0 & p = c%:MP) (msize p == 1%N).
proof: Proof. apply: (iffP eqP)=> [pC|[c nz_c ->]]; last by rewrite msizeC nz_c. have def_p: p = (p@_0)%:MP by rewrite -msize1_polyC ?pC. by exists p@_0; rewrite // -(mpolyC_eq0 n) -def_p -msize_poly_eq0 pC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg