proposition: Lemma zmap_setP a b: exists s, forall f, zmap f a b <-> inc f s.
proof: Proof. exists (Zo (\Po (zprod2 a b)) (fun z => zmap z a b)). move=> f; split; last by move => /Zo_P []. by move => h; apply /Zo_P;split => //; apply /setP_P;move: h => []. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)