proposition: Lemma olexp_worder: worder olexp.
proof: Proof. move: olexp_osr => [qa sa]; split => //. rewrite sa => X Xr neX. ex_middle not_least. have qb: sub X (substrate olexp) by rewrite sa. pose Pa Y:= [/\ sub Y X, nonempty Y & (forall x y, inc x Y -> inc y (X -s Y) -> glt olexp x y)]. have pa1: forall Y, Pa Y -> forall z, ~least (induced_order olexp Y) z. move => Y [pa pb pc] z => pd; case: not_least; exists z. move: pd; rewrite /least iorder_sr// ; last by apply: (sub_trans pa qb). move => [pd pe]; have zX: inc z X by apply: pa. rewrite iorder_sr //. split => //;move=> x xX; apply/iorder_gle0P => //;case: (inc_or_not x Y) => xY. move: (pe _ xY) => pf; apply: (iorder_gle1 pf). have xc: inc x (X -s Y) by apply /setC_P. by move: (pc _ _ pd xc) => [ok _]. pose Ja x A := (olexp_I x) -s A. pose Ma x A := the_greatest (induced_order r' (Ja x A)). have or': order r' by move: wor' => []. have or: order r by move: wor => []. have pa2: forall x A, inc x X -> sub (Ja x A) (substrate r'). move => x A xX. have s1: sub (Ja x A) (olexp_I x) by rewrite /Ja; move=> t /setC_P []. apply: (sub_trans s1); apply: Zo_S. have pa3: forall x A, inc x X -> nonempty (Ja x A) -> greatest (induced_order r' (Ja x A)) (Ma x A). move => x A xX neA. have s1: sub (Ja x A) (olexp_I x) by rewrite /Ja; move=> t /setC_P []. move: (Xr _ xX) => /Zo_P [_ fs2]. have fs: finite_set (Ja x A) by apply (sub_finite_set s1 fs2). have j1: sub (Ja x A) (substrate r') by apply: (pa2 _ _ xX). move: (iorder_osr or' j1) => [or1 sr1]. apply: the_greatest_pr => //. apply: finite_subset_torder_greatest => //. by apply : worder_total. have pa3': forall x A, inc x X -> nonempty (Ja x A) -> (inc (Ma x A) (Ja x A) /\ (forall k, inc k (Ja x A) -> gle r' k (Ma x A))). move => x A xX aux; move: (pa3 _ _ xX aux) => []. rewrite iorder_sr //; last by apply: pa2. move=> xx sb;split => // k ks; move: (sb _ ks) => sc;apply: (iorder_gle1 sc). pose ra Y A := induced_order r' (fun_image Y (fun z => Ma z A)). pose Aa Y A := the_least (ra Y A). pose Pb1 Y A := forall x, inc x Y -> nonempty (Ja x A). pose Pb2 Y A := forall x y i, inc x Y -> inc y Y -> inc i A -> Vg x i = Vg y i. pose Pb3 Y A := forall x i, inc x Y -> inc i (olexp_I x) -> inc i A \/ (forall j, inc j A -> glt r' i j). pose Ba Y A := Zo Y (fun z => Ma z A = Aa Y A). pose Ca Y A := fun_image (Ba Y A) (fun z => Vg z (Aa Y A)). pose Da Y A := the_least (induced_order r (Ca Y A)). pose Za Y A := Zo (Ba Y A) (fun z => Vg z (Aa Y A) = Da Y A). pose Ta Y A := A +s1 (Aa Y A). pose Pc Y A := [/\ Pa Y, Pb2 Y A, sub A (substrate r') & Pb3 Y A]. pose Pb4 Y A := forall i, inc i A -> glt r' (Aa Y A) i. have H0: Pc X emptyset. split => //. - by split => //; move=> x y _ /setC_P []. - by move=> x y i _ _ /in_set0. - fprops. - by move => x i _ _; right; move => j /in_set0. set f := induction_term (fun n p => J (Za (P p) (Q p)) (Ta (P p) (Q p))) (J X emptyset). have f0: f \0c = J X emptyset by apply: induction_term0. have fn: forall n, inc n Nat -> let Y := P (f n) in let A := Q (f n) in f (csucc n) = J (Za Y A) (Ta Y A). by move => n nB; simpl; rewrite /f induction_terms. suff HP: forall Y A, Pc Y A -> ( Pc (Za Y A) (Ta Y A) /\ Pb4 Y A). have fp: forall n, inc n Nat -> Pc (P (f n)) (Q (f n)). apply: Nat_induction; first by rewrite f0; aw. move=> n nB hrec; move: (fn _ nB); simpl; move => ->; aw. by move: (HP _ _ hrec) => []. pose g n := Aa (P (f n)) (Q (f n)). move: Nat_order_wor => []. set r'':= Nat_order => wor'' wsr. have Ai:forall i j, i <=N j -> sub (Q (f i)) (Q (f j)). move=> i j [iB jB ij]. move:(NS_diff i jB) (cdiff_pr ij). set k:= j -c i; move=> kB <-; move: k kB. apply: Nat_induction; first by rewrite csum0r; fprops. move=> n nB => hrec; apply: (sub_trans hrec); rewrite csum_nS //. by rewrite fn /Ta; aww; apply:NS_sum. have gp: forall n, inc n Nat -> inc (g n) (Q (f (csucc n))). by move=> n nB; rewrite (fn _ nB); aw; apply /setU1_P; right. have gpr: forall i j, inc i Nat-> inc j Nat -> i<c j -> inc (g i) (Q (f j)). move => i j iB jB /(cleSltP iB) sij. move: (gp _ iB) => h. have aux: (csucc i <=N j) by split;fprops. exact : ((Ai _ _ aux) _ h). have gnp: forall n, inc n (substrate r'') -> inc (g n) (substrate r'). rewrite wsr; move => n nB; move: (gp _ nB). move: (fp _ (NS_succ nB))=> [p1 p2 p3 p4]; by move: p3; apply. have gp1: forall i j, glt r'' i j -> glt r' (g j) (g i). move=> i j lij. have [iB jB ij]: [/\ inc i Nat, inc j Nat & i <c j]. move: lij => [] /Nat_order_leP [pa pb pc] pd; done. move: (gpr _ _ iB jB ij); move: (fp _ jB) => pci. move: (HP _ _ pci) => [_]; apply. move: (worder_decreasing_finite wor'' wor' gnp gp1); rewrite wsr. by move: infinite_Nat_alt. have pa0: forall Y y i, Pa Y -> inc y Y -> inc i (substrate r') -> inc (Vg y i) (substrate r). move => Y y i [pa _ _] yY isr. move: (Xr _ (pa _ yY)) => /Zo_P [] /gfunctions_P2 [sa' sb sc] _. apply sc; apply /(range_gP sa'); rewrite sb; ex_tac. move=> Y A [pa pb pra prb]; move: (pa) =>[sYX neY xynY]. have sy: sub Y (substrate olexp) by apply: (sub_trans sYX qb). have hp1: Pb1 Y A. move=> x xY; case: (emptyset_dichot (Ja x A)) => //. move=> je; case: (pa1 Y pa x); red; rewrite iorder_sr //. split => // y yY; apply /iorder_gleP => //. have aux: forall i, inc i (substrate r') -> gle r (Vg x i) (Vg y i). move => i isr; move: (pa0 Y y i pa yY isr) => vis. case: (inc_or_not i (olexp_I x)) => iI. have iA: inc i A. ex_middle niA; empty_tac1 i; apply /setC_P;split => //. by rewrite (pb _ _ _ xY yY iA); order_tac. move: iI => /Zo_P sa'. have ->: Vg x i = olexp_lE by ex_middle xx; case: sa';split => //. have xx: (nonempty (substrate r)) by exists (Vg y i). move: (olexp_lEp xx) => [_ sd]; apply: sd => //. move: olexp_total => to; case: (total_order_pr2 to(sy _ yY) (sy _ xY)) => //. move=> [lexy nxy]; move: lexy => /olexp_gleP [_ _ h]. case: h => //;move=> [j [jsr vxy _]]; move: (aux _ jsr) => vyx; order_tac. have pa4: least (ra Y A) (Aa Y A). rewrite /ra; set T := fun_image _ _. have neT: nonempty T. move: neY => [y yY]; exists (Ma y A); apply /funI_P; ex_tac. have sT: sub T (substrate r'). move => t /funI_P [z zY ->]. move: (pa3' _ _ (sYX _ zY) (hp1 _ zY)) => [pg ph]. by move: (pa2 z A (sYX _ zY)); apply. apply the_least_pr. by apply: (proj1 (iorder_osr or' sT)). move: wor' => [_ ok]; apply: ok => //. have pa5: sub (fun_image Y (Ma^~ A)) (substrate r'). move=> t /funI_P [z zY ->]. have zX: inc z X by apply: sYX. move: (pa2 z A zX) => sr2. by move: (pa3' _ _ zX (hp1 _ zY)) => [h1 _]; apply: sr2. have pa6: inc (Aa Y A) (fun_image Y (Ma^~ A)). move: pa4 => []; rewrite /ra iorder_sr //. have pa7: inc (Aa Y A) (substrate r') by move: pa5 pa6; apply. have neC: nonempty (Ca Y A). move: pa6 => /funI_P [z z1 z2]. by exists (Vg z (Aa Y A)); apply /funI_P;exists z => //; apply: Zo_i. have pa8: sub (Ca Y A) (substrate r). move=> t /funI_P [z z1 ->]. move: pa7 z1 => ais /Zo_P [zy _]. by apply: (pa0 Y z (Aa Y A)) => //; move: pa => [pa _]. have pa9: least (induced_order r (Ca Y A)) (Da Y A). apply: the_least_pr. apply: (proj1 (iorder_osr or pa8)) => // t; rewrite /Ca; aw. by move: wor => [_ wor1]; apply: wor1; [apply: pa8 | apply: neC ]. have s1: (sub (Ba Y A) Y) by apply: Zo_S. have sZY: sub (Za Y A) Y by apply: sub_trans s1; apply: Zo_S. have neZ: nonempty (Za Y A). move: pa9 => []; rewrite iorder_sr //; move /funI_P. move=> [z zb vz] _; exists z; apply: Zo_i => //. have pa10: forall x y, inc x (Za Y A) -> inc y (X -s (Za Y A)) -> glt olexp x y. move=> x y xZ => /setC_P [yX yc]. have nxy : x <> y by dneg xy; ue. move: xZ => /Zo_P [] /Zo_P [xY se] sf. have xX: inc x X by exact (sYX _ xY). case: (inc_or_not y Y) => yY; last by apply:xynY => //;apply/setC_P. split => //; apply /olexp_gleP; split;fprops; right. have sm: gle r' (Aa Y A) (Ma y A). move: pa4 => []; rewrite /ra iorder_sr //. move => _ h. have mf: inc (Ma y A) (fun_image Y (Ma ^~ A)) by apply /funI_P; ex_tac. by move: (h _ mf) => le1; move: (iorder_gle1 le1). have sd : forall i : Set, glt r' (Ma y A) i -> Vg x i = Vg y i. move => k kp. case: (inc_or_not k A) => kA; first by apply: pb => //. case: (equal_or_not (Vg y k) olexp_lE). move => ->; ex_middle vx. have kJ: inc k (Ja x A). apply: Zo_i => //; apply: Zo_i => //; order_tac. move: (pa3' _ _ xX (hp1 _ xY)) => [sg sh]. move: (sh _ kJ) => si. have lt1: glt r' (Ma y A) (Ma x A) by order_tac. have : glt r' (Aa Y A) (Ma x A) by order_tac. by rewrite se; move=> [_]. move => aux3. have kJ: inc k (Ja y A). apply: Zo_i => //; apply: Zo_i => //; order_tac. move: (pa3' _ _ yX (hp1 _ yY)) => [_ sh]; move: (sh _ kJ) => ?; order_tac. case: (inc_or_not y (Ba Y A)). move=> yB; move: yc => /Zo_P bad1. case:(equal_or_not (Vg y (Aa Y A)) (Da Y A)) => eq1; first by case: bad1. move: pa9 => []; rewrite iorder_sr //. move=> sa' sb. have vc: inc (Vg y (Aa Y A)) (Ca Y A) by apply /funI_P; ex_tac. move: (sb _ vc) => aux; move: (iorder_gle1 aux) => aux2. have lt1: glt r (Vg x (Aa Y A)) (Vg y (Aa Y A)). by rewrite sf;split => //; apply:nesym. exists (Aa Y A);split => //. move: yB => /Zo_P [_ sc]; rewrite - sc. apply: sd; rewrite sc; order_tac. rewrite /Ba => /Zo_P ny. case: (equal_or_not (Ma y A) (Aa Y A)) => sm1; first by case: ny. exists (Ma y A);split => //; first by order_tac. move: (pa3' _ _ xX (hp1 _ xY)) => [sa' sb]. move: (pa3' _ _ yX (hp1 _ yY)) => [say sby]. case: (inc_or_not (Ma y A) (Ja x A)) => le1. move: (sb _ le1); rewrite se => le2; case: sm1; order_tac. have nsv: (Vg x (Ma y A)) <> (Vg y (Ma y A)). move: say => /Zo_P [sg sh]. move: le1 => /Zo_P si. case: (inc_or_not (Ma y A) (olexp_I x)) => h; first by case: si. move: h sg => /Zo_P sj /Zo_P [sk sl]. move=> sn; case: sj; rewrite sn; split; exact. split => //. case: (equal_or_not (Vg x (Ma y A)) olexp_lE). move => ->. have isr: inc (Ma y A) (substrate r') by order_tac. move: (pa0 Y y (Ma y A) pa yY isr) => vis. have xx: (nonempty (substrate r)) by exists (Vg y (Ma y A)). move: (olexp_lEp xx) => [_ sg]; apply: sg => //. case: (inc_or_not (Ma y A) A) => ma; first by case: nsv; apply: pb. move => nsve. have kJ: inc (Ma y A) (Ja x A). apply: Zo_i => //; apply: Zo_i => //; order_tac. move: (sb _ kJ); rewrite se => lt1; case: sm1; order_tac. have pa12:Pb2 (Za Y A) (Ta Y A). move=> x y i. move /Zo_P => [xB sxV]. move /Zo_P => [yB syV]. case/setU1_P; last by move => ->; rewrite sxV syV. by apply: pb; apply: s1. have pa11: sub (Ta Y A) (substrate r'). move=> t; case /setU1_P; [by apply: pra | by move => ->]. have pay: Pa (Za Y A). split => //; first by apply: (sub_trans sZY). have pa13: Pb3 (Za Y A) (Ta Y A). move => x i xZ iI. move: xZ => /Zo_P [] /Zo_P [x1 x2] x3. case: (prb _ _ x1 iI) => h; first by left; apply /setU1_P; left. case: (inc_or_not i A) => iA; first by left; apply /setU1_P; left. case: (equal_or_not i (Aa Y A)) => ia; first by left; apply /setU1_P;right. right => j; case /setU1_P; first by apply: h. move=> ->; split => //; rewrite -x2. move: (pa3' _ _ (sYX _ x1) (hp1 _ x1)) => [say sby]. by apply: sby; apply Zo_i. have//: Pb4 Y A. move=> i iA. move: pa4; move=> []; rewrite iorder_sr //. move /funI_P=> [z zY zv]. move: (pa3' _ _ (sYX _ zY) (hp1 _ zY)) => [say sby]. move: say => /Zo_P [p1 p2]. case: (prb _ _ zY p1) => //. by rewrite - zv; move=> h _; apply h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)