proposition: Lemma zequiv_example2 a b c d: let A := doubleton a b in let B := doubleton c d in disjoint A B -> a <> b -> c <> d -> ziequivalent A B.
proof: Proof. move=> A B dAB nab ncd; split => //. exists (doubleton (doubleton a c) (doubleton b d)); by apply: zmap_example2. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)