proposition: Lemma dinsupp_dlet f mu y : y \in dinsupp (\dlet_(x <- mu) f x) -> exists2 x, x \in dinsupp mu & f x y != 0.
proof: Proof. move/dinsuppP; rewrite dletE => /neq0_psum [x /eqP]; rewrite mulf_eq0. by case/norP=> /eqP/dinsuppPn mux nz_fxy; exists x. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum