proposition: Lemma msuppM_le g1 g2 k : k \in msupp (g1 * g2) -> exists k1 k2, [/\ k1 \in msupp g1, k2 \in msupp g2 & k = (k1 * k2)%M].
proof: Proof. move/msuppM_le_finType => [] [k1 Hk1] [] [k2 Hk2] /= Hk. by exists k1; exists k2. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap