proposition: Lemma ex5_res3 F k (f := (ex5_f j k)) (T:= Vfs f ((Vg Gf k) \cap (ex5_Y F k (restr x F)))): ex5_b_prop F k -> nonempty T /\ T = Zo (Vg Gf j) (fun t => gle (Vg Er j) t (Vf f (ex5m F k (restr x F)))).
proof: Proof. move => [fnsFJ ubKn lejk]. move: ((proj33 coh2) _ fnsFJ) => co1. move:(prl_prop0 lejk) => [jI kI]. move:(prl_prop4 lejk) => [fjk sjk tjk]. have pa: sub (Vg Gf k) (source (ex5_f j k)). by move => t; rewrite sjk; apply:ex5_G4. have pb:= (sub_trans (@setI2_1 (Vg Gf k) (ex5_Y F k (restr x F))) pa). split; first by apply: (nonempty_image fjk _ pb); exact: (proj44 co1 _ ubKn). have pc:=(ex5_res1b co1 ubKn). set_extens t. move/(Vf_image_P fjk pb)=> [u uGY ->]. move /setI2_P:(uGY) => [/(ex5_Gij_prop1 lejk) uG uY]. move: uGY; rewrite pc => /Zo_P [_ le1]. by apply/Zo_P; split => //; move:(fm lejk) => [or1 or2 _]; aw; apply. move => /Zo_P [tG le1]. have mE:=(ex5m_prop4 (proj41 co1) ubKn (proj42 co1)). have hh: exists2 y, inc y (Vg Gf k) & gle (Vg Er k) y (ex5m F k (restr x F)). move:(proj44 co1 _ ubKn). rewrite pc; move => [y /Zo_P [ya yb]]; ex_tac. move:(ex5_G8 lejk mE hh tG le1) => [x' [x'G le2 vv]]. apply/(Vf_image_P fjk pb); rewrite pc. by exists x' => //; apply/Zo_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)