proposition: Lemma le1_mu1 {R : realType} {T : choiceType} (mu : {distr T / R}) x : mu x <= 1.
proof: Proof. apply/(@le_trans _ _ (psum mu)) => //; rewrite -[mu x]ger0_norm//. by apply/ger1_psum. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum