proposition: Lemma orprod_gle1P r g: orprod_ax r g -> forall x x', (related (order_prod r g) x x' <-> [/\ inc x (prod_of_substrates g), inc x' (prod_of_substrates g) & forall j, least (induced_order r (Zo (domain g) (fun i => Vg x i <> Vg x' i))) j -> glt (Vg g j) (Vg x j)(Vg x' j)]).
proof: Proof. move=> ax x x';apply/graph_on_P1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)