proposition: Lemma zmap_aux_pr2 f a b x y: zmap f a b -> inc x (a \cup b) -> inc y f -> inc x y -> y = (zmap_aux f x).
proof: Proof. move => zm xu yf xy;move: (zmap_aux_pr1 zm xu) => [pa pb]. move: zm=> [_ pc]; move: (pc _ xu) => [z [zx unq]]. by rewrite - (unq _ (conj yf xy)) (unq _ (conj pa pb)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)