proposition: Lemma zequiv_example1 a b: a <> b -> ziequivalent (singleton a) (singleton b).
proof: Proof. move=> ab; split; first by apply: disjoint_pr => u /set1_P -> /set1_P. exists (singleton (doubleton a b)); apply: (zmap_example1 ab). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)