proposition: Lemma mmapZ c g : (c *: g)^[f,h] = f c * g^[f,h].
proof: Proof. rewrite (mmapEw (msuppZ_le _ _)) mmapE big_distrr /=. by apply/eq_bigr=> k _; rewrite linearZ rmorphM /= mulrA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap