proposition: Lemma msize1_polyC p : msize p <= 1 -> p = (p@_0)%:MP.
proof: Proof. move=> le_p_1; apply/mpolyP=> m; rewrite mcoeffC. case: (m =P 0%MM)=> [->|/eqP]; first by rewrite mulr1. rewrite mulr0 -mdeg_eq0 => nz_m; rewrite memN_msupp_eq0 //. by apply/msize_mdeg_ge; rewrite 1?(@leq_trans 1) // lt0n. 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