proposition: Lemma orprod_gltP r g : orprod_ax r g -> forall x x', (glt (order_prod r g) x x' <-> [/\ inc x (prod_of_substrates g), inc x' (prod_of_substrates g) & exists j, [/\ inc j (substrate r), glt (Vg g j) (Vg x j) (Vg x' j) & forall i, glt r i j -> Vg x i = Vg x' i]]).
proof: Proof. move => ha x y; split => //. by move =>[/ (orprod_gleP ha) [qa qb qc] qd]; split => //; case: qc. move =>[qa qb qc]; split. by apply/ (orprod_gleP ha); split => //; right. by move => ea; move: qc =>[j [ _ /proj2]]; rewrite ea. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)