proposition: Lemma __deprecated__dsndE (mu : {distr (T * U) / R}) y : dsnd mu y = psum (fun x => mu (x, y)).
proof: Proof. by rewrite -__deprecated__dfst_dswap dfstE; apply/eq_psum=> x; rewrite dswapE. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum