proposition: Lemma gfunctions_hi x y z: inc z (gfunctions x y) -> exists f, [/\ function f, source f = x, target f = y & graph f = z].
proof: Proof. move/Zo_P => [/setP_P /corr_propcc [_ _ pa] [pb pc]]. exists (triple x y z); aw; split => //; apply: function_pr=>//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)