proposition: Lemma rpred_meval : {in monalgOver S, forall g (v : K -> R), (forall x, v x \in S) -> mmap idfun v g \in S}.
proof: Proof. move=> g /monalgOverP Sg v Sv; rewrite mmapE rpred_sum //. by move=> /= k; rewrite rpredM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap