proposition: Lemma fgmullw (d1 d2 : {fset K}) g1 g2 : msupp g1 `<=` d1 -> msupp g2 `<=` d2 -> fgmul g1 g2 = \sum_(k1 <- d1) \sum_(k2 <- d2) g1 *M_[k1, k2] g2.
proof: Proof. move=> le_d1 le_d2; rewrite fgmull (big_fset_incl _ le_d1) /=. apply/eq_bigr=> k1 _; apply/big_fset_incl => // k _ /mcoeff_outdom ->. by rewrite mulr0 monalgU0. move=> k _ /mcoeff_outdom g1k. by rewrite big1 => // k' _; rewrite g1k mul0r monalgU0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap