proposition: Lemma zmap_aux_pr1 f a b x: zmap f a b -> inc x (a \cup b) -> (inc (zmap_aux f x) f /\ inc x (zmap_aux f x)).
proof: Proof. move=> [pa pb] xu; move: (pb _ xu) => [u [[ta tb] pd]]. have h: singl_val2 (inc^~ f) (fun z => inc x z). by move => t y sa sb sc sd; rewrite -(pd _ (conj sa sb)) -(pd _ (conj sc sd)). rewrite /zmap_aux - (select_uniq h ta tb);split => //. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)