proposition: Lemma __deprecated__dsnd_dswap : dsnd (dswap mu) =1 dfst mu.
proof: Proof. move=> z; rewrite __deprecated__dlet_dlet; apply/eq_in_dlet => // -[x y]. by move=> _ t /=; rewrite dlet_unit /=. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum