proposition: Lemma mmapU (c : G) (m : K) : mmap f h << c *g m >> = f c * h m.
proof: Proof. by rewrite (mmapEw msuppU_le) big_seq_fset1 mcoeffUU. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap