proposition: Lemma zmap_example3 F a b: disjoint a b -> zbijective F a b -> ziequivalent a b.
proof: Proof. move=> dab [pa pb pc]; split => //. set (f := Zo (\Po (union2 a b)) (fun z => exists2 x, inc x a & z = doubleton x (F x))). red in dab. exists f; split. move=> t => /Zo_P [] /setP_P tu [x xa td]; apply /zprod2_P. move: (pa _ xa)=> fb; split => //. apply: (@is_singleton_int _ _ x) => //; first by rewrite td;fprops. rewrite td => u;case/set2_P =>// qa qb; empty_tac1 u. apply /setI2_P;split => //;ue. apply: (@is_singleton_int _ _ (F x)) => //; first by rewrite td;fprops. rewrite td => u; case /set2_P =>// qa qb; empty_tac1 u. apply /setI2_P;split => //;ue. move=> x; aw => xu; apply /unique_existence; split. case /setU2_P: xu => xu. exists (doubleton x (F x)); split; last by fprops. apply: Zo_i; last by ex_tac. apply /setP_P;move => t;case /set2_P=> ->; [ fprops | apply /setU2_P]. by right; apply: pa. move: (pc _ xu)=> [z za Fz]; exists (doubleton z x);split;fprops. apply: Zo_i; first by apply /setP_P;move=> t; case /set2_P=> ->; fprops. ex_tac; ue. move=> u v [uf xz] [yf xy]. move: uf yf => /Zo_P [] /setP_P uu [z za zu] /Zo_P [] /setP_P vy [w wa vw]. move: xz xy;rewrite zu vw; case /set2_P => xpa; case /set2_P=> xpb. - by rewrite -xpa -xpb. - by empty_tac1 x; apply /setI2_P;split => //; ue. - by empty_tac1 x; apply /setI2_P; split => //; ue; rewrite xpa; apply: pa. - by rewrite xpa in xpb; rewrite (pb _ _ za wa xpb). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)