proposition: Lemma mmap_is_additive : additive (mmap f h).
proof: Proof. move=> g1 g2 /=; pose_big_fset K E; rewrite 3?(mmapEw (d := E)) //. by rewrite -sumrB; apply/eq_bigr=> k _; rewrite !raddfB /= mulrBl. by close. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap