proposition: Lemma graph_fb x y: bijection (Lf graph (functions x y) (gfunctions x y)).
proof: Proof. apply: lf_bijective. - by apply: graph_lf_axiom. - by move=> u v us vs g; apply: (function_exten5 us vs g). - move=> z /gfunctions_hi [f [pa pb pc pd]]. by exists f => //;apply/functionsP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)