proposition: Lemma order_graph_osr: order g -> order_on (order_graph x y g) (gfunctions x y).
proof: Proof. move=> og; rewrite order_graph_pr =>//. have [pa pb] := (order_product_osr (order_fam_cst og (x:=x))). by split => //; rewrite order_graph_pr1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)