proposition: Lemma dlet_null f : dlet f dnull =1 dnull.
proof: Proof. move=> x; rewrite dletE dnullE /= /mlet psum_eq0 //. by move=> y; rewrite dnullE mul0r. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum