proposition: Lemma zmap_val_pr2a f a b x: zmap f a b -> inc x a -> (zmap_val f a x) = x.
proof: Proof. move => cx xa. have xu: (inc x (union2 a b)) by apply: setU2_1. move : (zmap_aux_pr1 cx xu) => [zf xz]; move: cx => [pa pb]. symmetry; apply: (zprod2_pr1a (pa _ zf) xa xz). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)