proposition: Lemma msizeZ_proper (p : {mpoly R[n]}) c : c * mleadc p != 0 -> msize (c *: p) = msize p.
proof: Proof. have [->|nz_p] := eqVneq p 0; first by rewrite mleadc0 mulr0 eqxx. have [->|nz_c] := eqVneq c 0; first by rewrite mul0r eqxx. move=> h; rewrite -[msize p]mlead_deg // -(mleadZ_proper h). rewrite mlead_deg //; pose m := (mlead p); apply/negP. move/eqP/(congr1 (mcoeff m)); rewrite mcoeffZ mcoeff0. by move/eqP; rewrite (negbTE h). 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