proposition: Lemma ex5_res1b J k x: ex5_coherent1 J x -> ex5_upper_bd J k -> (Vg Gf k) \cap (ex5_Y J k x) = Zo (Vg Gf k) (fun y => gle (Vg Er k) y (ex5m J k x)).
proof: Proof. move => ha ku. move:(ex5_res1a ha ku) => mp. move: ha => [fneI co2 si _]. have ru:= (ex5m_prop4 fneI ku co2). have Ha:=(ex5_Y_prop2 x (proj33 fneI) ku). have kI:= (proj1 ku). move:(ex5_Y_prop1 ku (x:=x)); rewrite - (sEr kI) => hu. case: mp; rewrite (iorder_sr (proj1 (lEr kI)) hu) => imY co3. set_extens t. by move/setI2_P => [ta /co3/iorder_gle1 tb]; apply/Zo_P. move/Zo_P => [ta tb]; apply/setI2_P;split => //. apply/Ha; split => //; first by apply: ex5_G4. move => i iJ. move:(proj2 ku _ iJ) => lik. have iI:= (proj1 (prl_prop0 lik)). move:(fm lik); aw; move =>[ork ori] _ fincr. move:(ex5m_prop3_bis fneI ku co2 iJ) => le1. have le2: gle (Vg Er k) t (ex5_M i k (Vg x i)) by order_tac. symmetry;ex_middle bad. move:(fincr _ _ le2). rewrite (proj1 (ex5_Mij_pr2 lik (proj33 co2 i iJ))) => le3. by case:(ex5_G5 iI (ex5_Gij_prop1 lik ta) (proj33 co2 i iJ) bad); left. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)