proposition: Lemma msuppM_le p q : {subset msupp (p * q) <= [seq (m1 + m2)%MM | m1 <- msupp p, m2 <- msupp q]}.
proof: Proof. move=> m; rewrite -[_ \in _]negbK -mcoeff_eq0 mcoeffM=> nz_s. apply/memPn=> /= h; move: nz_s; rewrite big1 ?eqxx //=. case=> m1 m2 /=; pose m'1 : 'X_{1..n} := m1; pose m'2 : 'X_{1..n} := m2. move/eqP=> mE; case: (boolP (m'1 \in msupp p)); last first. by move/memN_msupp_eq0=> ->; rewrite mul0r. case: (boolP (m'2 \in msupp q)); last first. by move/memN_msupp_eq0=> ->; rewrite mulr0. rewrite {}/m'1 {}/m'2=> m2_in_q m1_in_p; absurd false=> //. move: (h m); rewrite eqxx; apply; apply/allpairsP=> /=. exists (m1 : 'X_{1..n}, m2 : 'X_{1..n}) => /=. by rewrite m1_in_p m2_in_q /=. 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