proposition: Lemma gt1_mset (U : set T) (r : R) : measurable U -> (1 < r)%R -> mset U r = [set: probability T R].
proof: Proof. move=> mU r1; apply/seteqP; split => // x/= _. by rewrite /mset/= (le_lt_trans (probability_le1 _ _)). Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)