proposition: Lemma olex_nsve1 x y: inc x (prod_of_substrates g) -> inc y (prod_of_substrates g) -> let r' := (olex_io r x y) in let i := the_least r' in x <> y -> worder r' -> least r' i.
proof: Proof. move => px py r' i pa pb. have or: order r by move: ax => [[ok _]_ ]. have pc: 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 nse: nonempty (substrate r'). by rewrite sr'; apply /nonemptyP; move /(olex_nsve px py). move: (worder_least pb nse) => [j jl]. move: (pb) => [qa1 _];move: (the_least_pr2 qa1 jl). by rewrite /i; move => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)