proposition: Lemma mmapEw (d : {fset K}) g : msupp g `<=` d -> g^[f, h] = \sum_(k <- d) f g@_k * h k.
proof: Proof. move=> le; rewrite [LHS](big_fset_incl _ le) => //= x xd /mcoeff_outdom ->. by rewrite raddf0 mul0r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap