proposition: Lemma zmap_transitive a b c: disjoint a c -> ziequivalent a b -> ziequivalent b c -> ziequivalent a c.
proof: Proof. move=> dac [dab [f zmf]] [dbc [g zmg]]. move: (zmap_bijective zmf) (zmap_bijective zmg) => [pa pb pc][pd pe pf]. set (f1 := zmap_val f b); set (f2 := zmap_val g c). set (h := fun x => f2 (f1 x)). suff : (zbijective h a c) by apply: (zmap_example3 dac). split => //; first by move=> x xa; apply: pd; apply: pa. fprops. move=> y yc; move: (pf _ yc) => [x xb xb1]. by move: (pc _ xb) => [u ua uv]; ex_tac; rewrite xb1 uv. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)