proposition: Lemma le_mu_dlet f mu nu : mu <=1 nu -> dlet f mu <=1 dlet f nu.
proof: Proof. move=> le_mu x; unlock dlet; rewrite /= /mlet. apply/le_psum/summable_mlet => y; rewrite mulr_ge0 //=. case: (mu y =P 0) => [->|]; first by rewrite mul0r mulr_ge0. by move=>/dinsuppPn=> h; rewrite ler_pM. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum