proposition: Lemma zmap_val_pr1a f a b x: zmap f a b -> inc x (a \cup b) -> inc (zmap_val f a x) a.
proof: Proof. move=> zm xu;move: (zmap_aux_pr1 zm xu) => [pc pd]. move: (zm) => [pa pb]; apply: (zprod2_pr0aa (pa _ pc)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)