proposition: Lemma zequiv_example4 M N: exists M', disjoint N M' /\ ziequivalent M M'.
proof: Proof. move: (disjointness1 M N) => [r [a pa pb]]. by exists (zprod2 M (singleton r)); split => //; apply: zmap_example4. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)