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