proposition: Lemma zmap_bijective f a b: zmap f a b -> zbijective (zmap_val f b) a b.
proof: Proof. move=> zm; rewrite /zbijective; split => //. move=> x xa; apply: (zmap_val_pr1b zm (setU2_1 b xa)). move=> x x' xa x'a sv; move: (f_equal (zmap_val f a) sv). rewrite zmap_val_pr3a // zmap_val_pr3a //. move=> y yb; exists ( zmap_val f a y). by apply: (zmap_val_pr1a zm); apply /setU2_2. by rewrite zmap_val_pr3b. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)