proposition: Lemma zequiv_symm a b: ziequivalent a b -> ziequivalent b a.
proof: Proof. move => []; rewrite /disjoint setI2_C; move=> h [f zf]. by move: (zmap_symm zf) => zf1; split => //; exists f. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)