proposition: Lemma dletC (mu : {distr T / R}) (nu : {distr U / R}) y : (\dlet_(_ <- mu) nu) y = (dweight mu) * (nu y).
proof: Proof. rewrite dletE /pr [_ * nu y]mulrC -psumZ //=; apply/eq_psum. by move=> /= x; rewrite mul1r mulrC. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum