proposition: Lemma ex5_res5: exists x', ex5_extend_prop x j x'.
proof: Proof. move:ex5_res4 => [F0 [k0 [Fk0p F0k0min]]]. move:jJ =>[jI jd]. move:(ex5_res3 Fk0p) => [[x' xe] xf]; exists x'. move:xe; rewrite xf => /Zo_P [xG' lexfm]. have Ha F k: ex5_b_prop F k -> exists u, [/\ inc u (Vg Gf k), inc u (ex5_Y F k (restr x F)) & x' = Vf (ex5_f j k) u]. move => hF. move: (F0k0min _ _ hF) => eq2. move: (proj43 (proj1 (lEr jI)) _ _ _ lexfm eq2) => lee. move: (prl_prop4 (proj33 hF)) =>[fjk sjk tjk]. move:(proj2 (ex5_res3 hF));set T := Zo _ _ => eqq. have kI:=(proj1 (proj32 hF)). have ss: (sub (Vg Gf k \cap ex5_Y F k (restr x F)) (source (ex5_f j k))). by rewrite sjk => t /setI2_P [/(ex5_G4 kI)]. have: inc x' T by apply/Zo_P. rewrite - eqq; move/(Vf_image_P fjk ss) =>[u /setI2_P [uG up] uv]. by exists u. clear xf lexfm F0k0min. have Hb i: inc i (domain x) -> gle (psr S) j i -> x' = Vf (ex5_f j i) (Vg x i). move => idx leij; move: (set1_1 i) => isi. have iI:= proj2 (prl_prop0 leij). have hu:ex5_upper_bd (singleton i) i. split => // t /set1_P ->. by apply:(proj32 (ps_preorder_r S) i); rewrite ps_substrate_r. have Hsi: ex5_b_prop (singleton i) i. split => //. + by split; [apply: set1_finite | apply:set1_ne | move => t /set1_P ->]. move:(Ha _ _ Hsi) => [u [ua ub uc]]. move/(ex5_Y_prop2 _ (set1_ne i) hu): ub => [uu hi]. move:(hi i (set1_1 i)); rewrite LgV//. by rewrite uc /ex5_f (ps_identity_f iI); rewrite idV // => ->. have Hc i: inc i (domain x) -> gle (psr S) i j -> (Vg x i) = Vf (ex5_f i j) x'. move => idx leij. have hu:ex5_upper_bd (singleton i) j by split => // t /set1_P ->. have Hsi: ex5_b_prop (singleton i) j. split => //. + by split; [apply: set1_finite | apply:set1_ne | move => t /set1_P ->]. + by apply:(proj32 (ps_preorder_r S) j); rewrite ps_substrate_r. move:(Ha _ _ Hsi) => [u [ua ub uc]]. rewrite uc /ex5_f (ps_identity_f jI). move/(ex5_Y_prop2 _ (set1_ne i) hu): ub => [uu hi]. move:(hi i (set1_1 i)); rewrite LgV// ? idV//; fprops. have xE': inc x' (Vg (psE S) j) by apply: ex5_G4. move: coh2 =>[[fgx _ xG] dxI co1xk]. have Vout:(Vg (ex5_extend x j x') j) = x' by rewrite (setU1_V_out _ fgx jd). have dsI:sub (domain (ex5_extend x j x')) (psI S). by rewrite domain_setU1; apply:setU1_sub. have ra:ex5_prodG (domain (ex5_extend x j x')) (ex5_extend x j x'). aw; split. + apply:fgraph_setU1 => //. + reflexivity. + rewrite domain_setU1 => i /setU1_P; case => iJ; last by rewrite iJ Vout. by rewrite (setU1_V_in _ fgx jd iJ); apply: xG. split => // K [fsK neK kJj]. have sKI:=(sub_trans kJj dsI). have rb:ex5_prodG K (restr (ex5_extend x j x') K). split => //; aww => i iK; rewrite LgV//; exact: (proj33 ra _ (kJj _ iK)). set K':= K -s1 j. case: (emptyset_dichot K') => kne. have jj:= (set1_1 j). have hj:Vg (restr (ex5_extend x j x') (singleton j)) j = x' by rewrite LgV//; ue. have Kv: K = singleton j. by apply:(set1_pr1 neK)=> t tK; ex_middle kj; empty_tac1 t; apply/setC1_P. split => //. rewrite Kv => j1 j2 /set1_P -> /set1_P -> lejj. rewrite hj /ex5_f ps_identity_f //; rewrite idV//. move => k [kI ljk1]; rewrite Kv. have ljk: gle (psr S) j k by apply: ljk1; rewrite Kv. move: (ex5_Gij_prop2 ljk xG') => [t ta tb]. have hh: ex5_upper_bd (singleton j) k by split => // i /set1_P ->. exists t; apply/setI2_P; split => //;apply/(ex5_Y_prop2 _ (set1_ne j) hh). split; first by apply:(ex5_G4 kI). by move => i /set1_P ->; rewrite hj. move: kJj; rewrite domain_setU1 => kJj. have KK: sub K' K by apply: sub_setC. have KJ':sub K' J' by move => t/setC1_P [ /kJj /setU1_P]; case. have fneK': finite_ne_sub K' J' by split => //; apply: sub_finite_set fsK. move:(co1xk _ fneK') =>[sa sb sc sd]. have Kp i: inc i K -> i <> j -> inc i J' by move/(kJj) => /setU1_P; case. split => //. move => j1 j2 j1K j2K lej1j2; rewrite !LgV//. case: (equal_or_not j1 j) => j1p;case: (equal_or_not j2 j) => j2p. + rewrite j1p j2p (setU1_V_out _ fgx jd). have kK: inc j K by ue. rewrite /ex5_f (ps_identity_f jI) idV//. + rewrite j1p (setU1_V_out _ fgx jd). have j2dx: inc j2 (domain x) by apply:Kp. rewrite (setU1_V_in _ fgx jd j2dx); apply: Hb => //; ue. + rewrite j2p (setU1_V_out _ fgx jd). have j1dx: inc j1 (domain x) by apply: Kp. rewrite (setU1_V_in _ fgx jd j1dx); apply: Hc => //; ue. + have j1dx: inc j1 (domain x) by apply: Kp. have j2dx: inc j2 (domain x) by apply:Kp. rewrite (setU1_V_in _ fgx jd j2dx) (setU1_V_in _ fgx jd j1dx). have j1K': inc j1 K' by apply/setC1_P. have j2K': inc j2 K' by apply/setC1_P. move:(sc _ _ j1K' j2K' lej1j2); rewrite ! LgV//. move => k. case: (inc_or_not j K) => jK; last first. rewrite -(setC1_eq jK) -/K'; move:(sd k) => qa qb. have ->: restr (ex5_extend x j x') K' = restr x K'. apply:fgraph_exten; aww => t tK'; rewrite ! LgV//. by rewrite (setU1_V_in _ fgx jd) //;apply: KJ'. exact: (qa qb). move => [kI ubk]. have ha': ex5_upper_bd K' k by split => //i /KK/ubk. have lejk: gle (psr S) j k by exact:(ubk _ jK). have ex5bp: ex5_b_prop K' k by split. move:(Ha K' k ex5bp) => [u [uG up uv]]. exists u; apply/setI2_P; split => //. apply/(ex5_Y_prop2 _ neK (conj kI ubk)). split; first by apply:(ex5_G4 kI). move => i iK; rewrite LgV//. case:(equal_or_not i j) => nij; first by rewrite nij Vout. have iK': inc i K' by apply/setC1_P. have idx: inc i (domain x) by apply: KJ'. rewrite (setU1_V_in _ fgx jd idx). move/(ex5_Y_prop2 _ kne ha'): up => [ssa ssb]. rewrite - (ssb _ iK'); rewrite LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)