proposition: Lemma mmeasure_sum (T : Type) (r : seq _) (F : T -> {malg G[M]}) (P : pred T) : (mmeasure (\sum_(i <- r | P i) F i) <= \max_(i <- r | P i) mmeasure (F i))%N.
proof: Proof. elim/big_rec2: _ => /= [|i k p _ le]; first by rewrite mmeasure0. apply: leq_trans (mmeasureD_le _ _) _; rewrite geq_max. by rewrite leq_maxl /= leq_max le orbC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap