proposition: Lemma zequiv_equipotent M N: zequiv M N <-> M \Eq N.
proof: Proof. have Ha: forall a b, ziequivalent a b -> a \Eq b. move => a b [dab [f zf]]. exists (Lf (zmap_val f b) a b); saw; apply:lf_bijective. - move => t ta; exact:(zmap_val_pr1b zf (setU2_1 b ta)). - move => u v ua va => zz. by rewrite - (zmap_val_pr3a zf ua) - (zmap_val_pr3a zf va) zz. - move => y yb; rewrite - (zmap_val_pr3b zf yb). have va:=(zmap_val_pr1a zf (setU2_2 a yb)); ex_tac. have Hb: forall x y, disjoint x y -> x \Eq y -> ziequivalent x y. move => x y dxy [f [[[ff ijf] [_ sjf]] sf tf]]. suff: zbijective (Vf f) x y by apply:zmap_example3. split. - move => t tx; Wtac. - by rewrite - sf. - by rewrite - sf - tf. split. move => [x xA xB]; exact: (EqT (Ha _ _ xA) (EqS (Ha _ _ xB))). move => MN. move: (zequiv_example4 M N) => [M' [h1 h2]]. exists M' => //; apply:(Hb _ _ h1); exact: (EqT (EqS MN) (Ha _ _ h2)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)