proposition: Lemma zmap_aux_pr3a f a b x y: zmap f a b -> inc x f -> inc y f -> zpr x a = zpr y a -> x = y.
proof: Proof. move=> zm xf yf szp; move: (zm) => [pa pb]. have zxu: (inc (zpr x a) (union2 a b)). by apply: setU2_1; apply: (zprod2_pr0aa (pa _ xf)). have zyu: (inc (zpr y a) (union2 a b)) by ue. rewrite (zmap_aux_pr2 zm zxu xf (zprod2_pr0ax (pa _ xf))). by rewrite (zmap_aux_pr2 zm zyu yf (zprod2_pr0ax (pa _ yf))) szp. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)