proposition: Lemma zmap_val_pr1b f a b x: zmap f a b -> inc x (a \cup b) -> inc (zmap_val f b x) b.
proof: Proof. move => zmf xu; move: (zmap_aux_pr1 zmf xu) => [zf xz]. move: zmf => [pa pb];move: (pa _ zf); apply: zprod2_pr0bb. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)