proposition: Lemma le_in_dlet f g mu : {in dinsupp mu, f <=2 g} -> dlet f mu <=1 dlet g mu.
proof: Proof. move=> le_f; unlock dlet=> y /=; apply/le_psum/summable_mlet. move=> x; rewrite mulr_ge0 //=; case: (mu x =P 0). by move=> ->; rewrite !mul0r. by move/dinsuppPn/le_f/(_ y) => 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