proposition: Lemma zmap_sub f a b a': zmap f a b -> sub a' a -> exists f' b', [/\ sub f' f, sub b' b & zmap f' a' b'].
proof: Proof. move=> zm saa. move: (zm) => [pa pb]. set (f' := Zo f (fun z => inc (zpr z a) a')). set (b':= Zo b (fun z => exists2 x, inc x f' & z = zpr x b)). have sf: sub f' f by apply: Zo_S. have sb: sub b' b by apply: Zo_S. exists f'; exists b'; split => //. have pc: (forall y, inc y f' -> y = doubleton (zpr y a) (zpr y b)). by move=> y yf'; apply: zprod2_pr2; apply: pa; apply: sf. split. move => x xf'. have ha: inc x (zprod2 a b) by apply: pa; apply: sf. have hb: (inc (zpr x a) a') by move: xf' => /Zo_P []. have hc: (inc (zpr x b) b') by apply: Zo_i; [apply:(zprod2_pr0bb ha)| ex_tac]. move: (zprod2_pr1 ha) => [pd pe]. apply /zprod2_P;split => //. rewrite (pc _ xf'); move=> t;case /set2_P => ->; fprops. apply: (@is_singleton_int _ _ (zpr x a)) => //. apply: (@setI2_1 _ a); rewrite pd; fprops. move=> u ux ua'. have : (inc u (x \cap a)) by fprops. by rewrite pd => /set1_P. apply: (@is_singleton_int _ _ (zpr x b)) => //. apply: (@setI2_1 _ b); rewrite pe; fprops. move=> u ux ua'. have : (inc u (x \cap b)) by fprops. by rewrite pe => /set1_P. move=> x xu. have xu': (inc x (a \cup b)) by move: xu; case /setU2_P => xs; fprops. move: (zmap_aux_pr1 zm xu') => [pd pe]; exists (zmap_aux f x); split. split => //; apply: Zo_i => //. move: xu; case /setU2_P => xs. by move: (zmap_val_pr2a zm (saa _ xs)); rewrite /zmap_val; move => ->. move: xs => /Zo_P [xb [z zf' xv]]. move: zf' => /Zo_P [pf pg]. have <- //: (z = zmap_aux f x). apply: (zmap_aux_pr2 zm xu' pf); rewrite xv; apply: (zprod2_pr0bx (pa _ pf)). move=> u [uf' ux]; move: (pb _ xu') => [z [zv zu]]. by rewrite - (zu _ (conj pd pe)) (zu _ (conj (sf _ uf') ux)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)