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