proposition: Lemma olexp_gle1P x y: inc x olexp_G -> inc y olexp_G -> (gle olexp' x y <-> ( x = y \/ (exists j, [/\ inc j (substrate r'), glt r (Vg x j) (Vg y j) & forall i, glt r' j i -> Vg x i = Vg y i]))).
proof: Proof. move: (wor') => [or' _] xG yG. move: (opp_osr or') => [or ssr]. move: (olexp_Gs xG) (olexp_Gs yG); set EF:= substrate olexp' => xE yE. have xe: inc x (prod_of_substrates olexp_g). by move: xE; rewrite /EF olex_sr. have ye: inc y (prod_of_substrates olexp_g). by move: yE; rewrite /EF olex_sr. apply: (iff_trans (olexp'_gleP _ _)). have ->: (gfunctions (substrate r') (substrate r)) = EF. by rewrite /EF (proj2 olexp'_osr). simpl; rewrite olexp_gleh. have hc:sub (olex_nsv (opp_order r') x y) (substrate (opp_order r')) by apply: Zo_S. have hd: (substrate (olex_io (opp_order r') x y)) = olex_nsv (opp_order r') x y. rewrite /olex_io iorder_sr //. case: (equal_or_not x y) => xy; first by (split => _; [| split => //]; left). move: ( olexp_Gxy1 xG yG) => pa. move: (olex_nsve1 olexp_ax xe ye xy pa). set j := the_least _ => jp. split. move => [_ _]; case; first (by left); move => [ha hb]; right. move: jp => []; rewrite hd => ja jb; exists j. move: ja => /Zo_P; rewrite ssr; move=> [jc jd]. split => // => i ij; ex_middle nsv. have pc: inc i (olex_nsv (opp_order r') x y). apply: Zo_i => //; rewrite ssr; order_tac. move: (jb _ pc)=> pc1; move:(iorder_gle1 pc1). move /opp_gleP => aux; order_tac. case; first by move => aux; contradiction. move=> [j0 [jsr jv ij]];split => //; right; split => //. have oi: order (olex_io (opp_order r') x y) by move: pa => []. suff jl: least (olex_io (opp_order r') x y) j0. by rewrite - (unique_least oi jl jp). have jsr1: inc j0 (olex_nsv (opp_order r') x y). by apply: Zo_i; rewrite ? ssr //; move: jv => []. red; rewrite hd; split => //. move=> k kp; move: (kp) => /Zo_P;rewrite ssr; move => [ksr sk]. rewrite /olex_io;aw;move: (worder_total wor') => tor. case: (total_order_pr2 tor jsr ksr) => lt1. move: (ij _ lt1) => eq1; contradiction. by apply/iorder_gle0P => //; apply/opp_gleP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)