proposition: Lemma order_graph_pr: order_graph x y g = order_product (cst_graph x g).
proof: Proof. rewrite /order_graph/order_product (order_graph_pr1) {2}/cst_graph. rewrite /graph_on/order_product_r Lgd. set_extens t => /Zo_P [t1 h]; apply /Zo_P;split =>// i ix; move: (h _ ix); rewrite LgV //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)