proposition: Lemma ex5_res4: exists F0 k0, ex5_b_prop F0 k0 /\ forall F k, ex5_b_prop F k -> gle (Vg Er j) (Vf (ex5_f j k0) (ex5m F0 k0 (restr x F0))) (Vf (ex5_f j k) (ex5m F k (restr x F))).
proof: Proof. pose mm F k := (Vf (ex5_f j k) (ex5m F k (restr x F))). have T := (proj33 (ps_preorder_r S)). have jI:= (proj1 jJ). have or:= (proj1 (lEr jI)). have hu F k k': ex5_b_prop F k -> gle (psr S) k k' -> ex5_b_prop F k'. move => [ff ubk lejk] lekk'. split=> //. split; first exact: (proj2 (prl_prop0 lekk')). move => i /(proj2 ubk) => la; exact:(T _ _ _ la lekk'). exact:(T _ _ _ lejk lekk'). have hv F k: ex5_b_prop F k -> inc (mm F k) (Vg (psE S) j). move => [ff ubk lejk]. have hb:=(proj33 coh2 F ff). move: ff=> [fsF neF sFJ]. have fne: ex5_fneI F by split => //; apply:(sub_trans sFJ (proj32 coh2)). have co2: ex5_prodG F (restr x F). split => //; aww => i iF; rewrite LgV//; apply:(proj33 (proj31 coh2)). by apply: sFJ. move:(ex5m_prop4 fne ubk co2) => me. by rewrite /mm/ex5_f; move: (prl_prop4 lejk) => [ff sf tf]; Wtac. have Ha F k k': ex5_b_prop F k -> gle (psr S) k k' -> gle (Vg Er j) (mm F k') (mm F k). move => pa lekk'; move:(proj32 (hu _ _ _ pa lekk')) => ubk'. move:pa => [ff ubk lejk]. have hb:=(proj33 coh2 F ff). move: ff=> [fsF neF sFJ]. have fne: ex5_fneI F by split => //; apply:(sub_trans sFJ (proj32 coh2)). have co2: ex5_prodG F (restr x F). split => //; aww => i iF; rewrite LgV//; apply:(proj33 (proj31 coh2)). by apply: sFJ. rewrite /mm -(prl_prop3 lejk lekk' (ex5m_prop4 fne ubk' co2)). move:(fm lejk); aw; move =>[ork orj _]; apply. move: (prl_prop0 lekk') =>[kI kI']. have ork' := (proj1 (lEr kI')). have sy1: sub (ex5_Y F k (restr x F)) (substrate (Vg Er k)). by rewrite (sEr kI); apply: ex5_Y_prop1. have sy2: sub (ex5_Y F k' (restr x F)) (substrate (Vg Er k')). by rewrite (sEr kI'); apply: ex5_Y_prop1. move: (ex5_res1a hb ubk) (ex5_res1a hb ubk'). set m := ex5m _ _ _; set m' := ex5m _ _ _. rewrite /greatest (iorder_sr ork sy1) (iorder_sr ork' sy2). move => [mY' maxm'][mY maxm]. suff ww: inc (Vf (Vg (psf S) (J k k')) m') (ex5_Y F k (restr x F)). exact: (iorder_gle1(maxm' (Vf (Vg (psf S) (J k k')) m') ww)). move: (prl_prop4 lekk') =>[fkk skk tkk]. have fkkmE: inc (Vf (Vg (psf S) (J k k')) m') (Vg (psE S) k). by Wtac; rewrite skk;move:(sy2 _ mY); rewrite (sEr kI'). apply /(ex5_Y_prop2 _ neF ubk); split => //. move => i iF; rewrite LgV//. move/(ex5_Y_prop2 _ neF ubk'): mY => [mu] h; move: (h _ iF); rewrite LgV//. by rewrite (prl_prop3 (proj2 ubk i iF) lekk' mu). have Hb: forall F F' k, ex5_b_prop F k -> ex5_b_prop F' k -> sub F F' -> gle (Vg Er j) (mm F' k) (mm F k). move => F F' k [ff ubk lejk] [ff' ubk' _] sff. move:(fm lejk); aw; move =>[ork orj _]; apply. have hb:=(proj33 coh2 F ff). have hb':=(proj33 coh2 F' ff'). have kI:= (proj1 ubk). move: (ex5_res1a hb ubk) (ex5_res1a hb' ubk'). have sy1: sub (ex5_Y F k (restr x F)) (substrate (Vg Er k)). by rewrite (sEr kI); apply: ex5_Y_prop1. have sy2: sub (ex5_Y F' k (restr x F')) (substrate (Vg Er k)). by rewrite (sEr kI); apply: ex5_Y_prop1. set m := ex5m _ _ _; set m' := ex5m _ _ _. rewrite /greatest (iorder_sr ork sy1) (iorder_sr ork sy2). move => [mY maxm][mY' maxm']. suff: inc m' (ex5_Y F k (restr x F)) by move/maxm => /iorder_gle1. move/(ex5_Y_prop2 (restr x F') (proj32 ff') ubk'): mY' => [qa qb]. apply/(ex5_Y_prop2 _ (proj32 ff) ubk); split => // i iF; rewrite LgV//. move:(sff _ iF) => iF'; rewrite -(qb _ iF'); rewrite LgV//. have Hc F F' k k': ex5_b_prop F k -> ex5_b_prop F' k' -> exists F'' k'', [/\ ex5_b_prop F'' k'', gle (Vg Er j) (mm F'' k'') (mm F k) & gle (Vg Er j) (mm F'' k'') (mm F' k')]. move => pa pb; move:(pa)(pb) => [ff ubk lejk] [ff' ubk' lejk']. move: (proj1 ubk) (proj1 ubk'); rewrite - ps_substrate_r => kr kr'. move:(rdr kr kr') =>[k'' [le1 le2]]. set F'' := F \cup F'. have neF'': nonempty F'' by move:(proj32 ff) =>[t tf]; exists t;apply:setU2_1. have ra: ex5_b_prop F'' k''. move:ff ff' =>[qa qb pc][pe pf pg]. split. + by split; [ apply:finite_U2 | exact | apply:setU2_12S]. + split; first exact:(proj2 (prl_prop0 le1)). move => i/setU2_P; case => ii. exact:(T _ _ _ (proj2 ubk _ ii) le1). exact:(T _ _ _ (proj2 ubk' _ ii) le2). + exact:(T _ _ _ lejk le1). set T'' := proj43 or. move:(Ha _ _ _ pa le1) (Ha _ _ _ pb le2) => la lb. move:(Hb F F'' k'' (hu F k k'' pa le1) ra (@subsetU2l F F')) => lc. move:(Hb F' F'' k'' (hu F' k' k'' pb le2) ra (@subsetU2r F F')) => ld. exists F'', k'';split => //. exact:(T'' _ _ _ lc la). exact:(T'' _ _ _ ld lb). set A := Zo (Vg (psE S) j) (fun z => exists F k, ex5_b_prop F k /\ z = mm F k). have Ap1: forall m m', inc m A -> inc m' A -> exists m'', [/\ inc m'' A, gle (Vg Er j) m'' m & gle (Vg Er j) m'' m']. move => m m' /Zo_P[mE [F [k [pa pb]]]] /Zo_P[mE' [F' [k' [pa' pb']]]]. move:(Hc _ _ _ _ pa pa') => [F'' [k'' [ra rb rc]]]. rewrite pb pb'; exists (mm F'' k''); split => //; apply/Zo_P; split. by move:(arg1_sr rb); rewrite (sEr jI). by exists F'', k''. have neA: nonempty A. move:Jne =>[i iJ]. have iI:= (proj32 coh2 _ iJ). move: iI jI; rewrite - ps_substrate_r => ir jr. move:(rdr ir jr) =>[k [le1 le2]]. have pp: ex5_b_prop (singleton i) k. split. + by split; [ apply: set1_finite | apply:set1_ne | apply:set1_sub]. + by split; [exact (proj2 (prl_prop0 le1)) | move => t /set1_P ->]. + exact. exists (mm (singleton i) k); apply:Zo_i; first by apply: hv. by exists (singleton i), k. have ap1: sub A (Vg (psE S) j) by apply: Zo_S. have ap2: sub A (substrate (Vg Er j)) by rewrite sEr. move:(sen jI ap1 neA) => [a[]]. rewrite (iorder_sr or ap2) => aA amin. move/Zo_P: (aA) => [aeJ [F [k [fkp ffv]]]]; exists F,k; split => //. move => F' k' fkp'; rewrite - /(mm F k) - ffv. have bA: inc (mm F' k') A by apply:Zo_i; [ by apply: hv | exists F', k']. move:(Ap1 _ _ aA bA) => [c [cA le1 le2]]. by move/(iorder_gle0P (Vg Er j) cA aA): le1 => /amin <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)