fact: Definition fgmullwl (d1 : {fset K}) {g1 g2} (le : msupp g1 `<=` d1) := @fgmullw _ _ g1 g2 le (fsubset_refl _).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap