proposition: Lemma dlet_dinsupp f mu x y : x \in dinsupp mu -> f x y != 0 -> y \in dinsupp (dlet f mu).
proof: Proof. move=> /dinsuppP /eqP mux nz_fxy; apply/dinsuppP; rewrite dletE. move/eq0_psum => /(_ (summable_mlet _ _ _) x) => /eqP. by rewrite mulf_eq0 (negbTE mux) (negbTE nz_fxy). Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum