proposition: Lemma olexp'_gleP x y: gle olexp' x y <-> [/\ inc x (gfunctions (substrate r') (substrate r)), inc y (gfunctions (substrate r') (substrate r)) & (x = y \/ let T := olex_nsv r' x y in let r'' := induced_order (opp_order r') T in worder r'' /\ let i := the_least r'' in glt r (Vg x i) (Vg y i))].
proof: Proof. set EF:= (prod_of_substrates olexp_g). apply: (iff_trans (olex_gleP _ _ _ _)). have ->: (gfunctions (substrate r') (substrate r)) = EF. by rewrite - (proj2 (olexp'_osr )) olex_sr. case: (equal_or_not x y) => exy. split; move => [pa pb pc];split => //; by left. have or': order r' by move: wor' => [ok _]. rewrite /olex_comp2_r /olex_comp1_r olexp_gleh. set q := (the_least (olex_io (opp_order r') x y)). move: (opp_osr or') => [oro sro]. have aux: inc x EF -> inc y EF -> worder (olex_io (opp_order r') x y) -> (Vg olexp_g q) = r. move => xe ye h; rewrite /olexp_g /cst_graph LgV//. move: (olex_nsve1 olexp_ax xe ye exy h); rewrite -/q; move => [pc _]. move: pc; rewrite iorder_sr //; last by apply: Zo_S. by move => /Zo_P []; rewrite sro. split; move=> [xE yE]; case => haux; split => //; right; move: haux; move => [wo1]; rewrite aux //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)