proposition: Lemma order_product_gleP g x x': (gle (order_product g) x x' <-> [/\ inc x (prod_of_substrates g), inc x' (prod_of_substrates g) & forall i, inc i (domain g) -> gle (Vg g i) (Vg x i)(Vg x' i)]).
proof: Proof. apply /graph_on_P0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)