proposition: Lemma dswapE xy : dswap mu xy = mu (xy.2, xy.1).
proof: Proof. rewrite dletE /= (psum_finseq (r := [:: (xy.2, xy.1)])) //. case=> a b; rewrite !inE dunit1E /= mulf_eq0. by case/norP=> _; rewrite pnatr_eq0 eqb0 negbK=> /eqP <-. by case: xy=> x y; rewrite big_seq1 dunit1E /= eqxx mulr1 ger0_norm. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum