proposition: Lemma msizeM_le (p q : {mpoly R[n]}) : msize (p * q) <= (msize p + msize q).+1.
proof: Proof. have [->|nz_p ] := eqVneq p 0; first by rewrite mul0r msize0. have [->|nz_q ] := eqVneq q 0; first by rewrite mulr0 msize0. have [->|nz_pq] := eqVneq (p * q) 0; first by rewrite msize0. rewrite -!mlead_deg // !(addSn, addnS) 2?ltnW // !ltnS. by have /lemc_mdeg := mleadM_le p q; rewrite mdegD. 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