proposition: Lemma olexp_Gxy x y: inc x olexp_G -> inc y olexp_G -> finite_set (olex_nsv (opp_order r') x y).
proof: Proof. move =>/Zo_P [pa pb] /Zo_P [pd pe]. have or': order r' by move: wor' => [ok _]. have pc: sub (olex_nsv (opp_order r') x y) ((olexp_I x) \cup (olexp_I y)). rewrite /olex_nsv /olexp_I => t /Zo_P; rewrite (proj2 (opp_osr or'))//. move => [pc h]; case: (equal_or_not (Vg y t) olexp_lE) => eq1; apply /setU2_P;[left | right]; apply : Zo_i => //; ue. by apply: (sub_finite_set pc); apply /finite_union2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)