proposition: Lemma dswapK : dswap (dswap mu) =1 mu.
proof: Proof. by case=> x y; rewrite !dswapE. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum