proposition: Lemma zmap_val_pr3b f a b x: zmap f a b -> inc x b -> (zmap_val f b (zmap_val f a x)) = x.
proof: Proof. move => zm; have: (zmap f b a) by apply: zmap_symm. apply: zmap_val_pr3a. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)