proposition: Lemma graph_of_function_is x y: order_isomorphism (graph_of_function x y) (opp_order (extension_order x y)) (sub_order (fgraphs x y)).
proof: Proof. have [eo sr]:= (extension_osr x y). have [sio sis] := (sub_osr (fgraphs x y)). have [ex sx]:= (opp_osr eo). hnf; rewrite /fiso_prop sis sx sr. have <- :sub_functions x y = source (graph_of_function x y). by rewrite /graph_of_function; aw. split; fprops. rewrite /graph_of_function; saw. by apply: graph_of_function_fb. move=> a b ass bss. rewrite graph_of_function_V // graph_of_function_V //. split. move /extension_order_P2 => [_ _ h]; apply/sub_gleP. by split => //; apply: set_of_graphs_pr. by move /sub_gleP => [pa pb pc]; apply /extension_order_P2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)