proposition: Lemma ex5_res1a J k x: ex5_coherent1 J x -> ex5_upper_bd J k -> greatest (induced_order (Vg Er k) (ex5_Y J k x)) (ex5m J k x).
proof: Proof. move => [fneI co2 si so] ku. have ru:= (ex5m_prop4 fneI ku co2). have Ha:=(ex5_Y_prop2 x (proj33 fneI) ku). have kI:= (proj1 ku). have orj:=(proj1 (lEr kI)). move:(ex5_Y_prop1 ku (x:=x)); rewrite - (sEr kI) => hu. have hv: (substrate (induced_order (Vg Er k) (ex5_Y J k x))) = ex5_Y J k x. by rewrite iorder_sr. have co3 t: inc t (ex5_Y J k x) -> gle (Vg Er k) t (ex5m J k x). move /Ha => [ta tb]; apply/(ex5m_prop3 fneI ku co2) => i iJ. have lik := (proj2 ku _ iJ). by apply: (proj2 (ex5_Mij_pr2 lik (proj33 co2 _ iJ)) _ ta); rewrite tb. move:(so k ku) => [x' /setI2_P [x'G x'Y]]. have x'E:= (ex5_G4 kI x'G). have co4: gle (Vg Er k) x' (ex5m J k x) by apply:co3. suff imY: inc (ex5m J k x) (ex5_Y J k x). hnf; rewrite hv; split => // t tY; apply/iorder_gleP; split; fprops. apply/Ha; split; [ apply: ru | move => i iJ]. move:(proj2 ku _ iJ) => lik. have iI:= (proj1 (prl_prop0 lik)). move:(fm lik); aw; move =>[ork ori] _ fincr. move:(fincr _ _ (ex5m_prop3_bis fneI ku co2 iJ)). move /(ex5_Y_prop2 _ (proj33 fneI) ku): x'Y => [_ x'p]. move:(fincr _ _ co4); rewrite - (x'p _ iJ). rewrite(proj1 (ex5_Mij_pr2 lik (proj33 co2 i iJ))) => qa qb; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)