proposition: Lemma msuppM_le_finType g1 g2 k : k \in msupp (g1 * g2) -> exists (k1 : msupp g1) (k2 : msupp g2), k = (val k1 * val k2)%M.
proof: Proof. move=> k_in_g1Mg2; apply/(existsPP (fun _ => exists_eqP)). apply/contraLR: k_in_g1Mg2=> hk; rewrite -mcoeff_eq0. rewrite mcoeffMl big_seq big1 // => /= k1 Hk1. rewrite big_seq big1 // => k2 Hk2. case: eqP=> // kE; case/negP: hk. by apply/existsP; exists [` Hk1]; apply/existsP; exists [` Hk2]; rewrite kE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap