proposition: Lemma zequiv_transitive M N P: zequiv M N -> zequiv N P -> zequiv M P.
proof: Proof. move=> [f fa fb] [g ga gb]. move: (zequiv_example4 f (g \cup (P \cup (M \cup N)))) => [h [hd he]]. red in hd. exists h => //. have d1: (disjoint M h) by apply: disjoint_pr => u uM uh; empty_tac1 u; aw. exact: (zmap_transitive d1 fa he). have d2: (disjoint N h) by apply: disjoint_pr => u uM uh; empty_tac1 u; aw. move: (zmap_transitive d2 fb he) => Nh. have d3: (disjoint g h) by apply: disjoint_pr => u uM uh; empty_tac1 u; aw. move: (zmap_transitive d3 (zequiv_symm ga) Nh) => gh. have d4: (disjoint P h) by apply: disjoint_pr => u uM uh; empty_tac1 u; aw. exact (zmap_transitive d4 gb gh). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)