proposition: Lemma olex_glt_aux x y (r' := olex_io r x y) (i := the_least r'): glt (olex r g) x y -> (inc i (substrate r) /\ forall j, glt r j i -> Vg x j = Vg y j).
proof: Proof. move => [h nxy] . move:h => /olex_gleP [pa pb]; case => pc; first by contradiction. move: pc => [wor]; move: (olex_nsve1 pa pb nxy wor). rewrite /= -/i; move => [pc pd] pe. have or: order r by move: ax => [[ok _]_ ]. have pf: sub (olex_nsv r x y) (substrate r) by apply: Zo_S. have sr': substrate r' = olex_nsv r x y by rewrite /r' iorder_sr. have pg: inc i (substrate r) by apply: pf; rewrite - sr'. split => //. move => k ki; ex_middle aux. have kp: inc k (substrate r') by rewrite sr' ; apply:Zo_i => //; order_tac. move: (pd _ kp); rewrite /r' => aux1; move: (iorder_gle1 aux1) => aux2. order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)