proposition: Lemma gfunctions_P1 a b z: inc z (gfunctions a b) <-> [/\ fgraph z, domain z = a & sub z (a \times b)].
proof: Proof. split; first by move/Zo_P => [/setP_P pa [pb pc]]. move => [pa pb pc]; apply: Zo_i; [by apply/setP_P | done]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)