proposition: Lemma order_function_is: order_isomorphism (Lf graph (functions x y)(gfunctions x y)) (order_function x y r)(order_graph x y r).
proof: Proof. have [pa pb]:= order_function_osr. have [pc pd] := order_graph_osr x sr or. split => //; first by split; aw => //;apply: graph_fb. have ax :=(graph_lf_axiom (x:=x) (y:=y)). hnf; aw=> a b ass bss; rewrite ! LfV//; split. move/order_functionP => [_ _ h];apply:Zo_i;aw;trivial. by apply:setXp_i; apply: ax. by move /Zo_hi;aw => xx; apply/order_functionP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)