proposition: Lemma dinsupp_swap xy : (xy.2, xy.1) \in dinsupp mu -> xy \in dinsupp (dswap mu).
proof: Proof. by move=> h; apply/dinsuppP; rewrite dswapE; apply/dinsuppPn. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum