proposition: Lemma eq0_dlet (mu : {distr T / R}) (F : T -> {distr U / R}) y : (\dlet_(x <- mu) F x) y = 0 -> forall x, x \in dinsupp mu -> F x y = 0.
proof: Proof. unlock dlet; rewrite /= /mlet => /eq0_psum h x /dinsuppP /eqP mu_x. have {}/h: summable (fun x => mu x * F x y). apply/(le_summable (F2 := mu)) => // z. by rewrite mulr_ge0 //= ler_piMr // le1_mu1. by move/(_ x)/eqP; rewrite mulf_eq0 (negbTE mu_x) /= => /eqP. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum