proposition: Lemma summable_snd (mu : {distr (T * U) / R}) y : summable (fun x => mu (x, y)).
proof: Proof. have := summable_fst (dswap mu) y; apply/eq_summable. by move=> x /=; rewrite dswapE. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum