proposition: Lemma order_function_is1: (order_function x y r) \Is (order_graph x y r).
proof: Proof. exists (Lf graph (functions x y) (gfunctions x y)). by apply: order_function_is. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)