proposition: Lemma ex6_fct_fs: surjection ex6_iso.
proof: Proof. apply:(lf_surjective ex6_fct_ax) => y /inductive_limit_hi. set i := Q _; set z := P _; move => [iI zE ->]. move:(iI); rewrite - ex6_prop3 - HJI => /setUb_P [j]; rewrite HJd. move => jL iJl. set x1 := (class (inl_equiv (ex6_systemi j)) (J z i)). set x := class (inl_equiv ex6_F) (J x1 j). have x1in: inc x1 (inductive_limit (inl_restr (ex6_prop4 jL))). rewrite /x1 (ex6_prop6a jL). apply: inl_class_in_lim => //; simpl; rewrite LgV//. have x1Fj: inc x1 (Vg (isE ex6_F) j) by simpl; rewrite LgV//; rewrite ex6_res0. have xs:inc x (inductive_limit ex6_F). by apply:(inl_class_in_lim (S:=ex6_F) jL). ex_tac; rewrite /ex6_fct. move:(inductive_limit_hi xs). set j' := Q (rep x); set x1' := P (rep x);simpl; move => [j'L]. rewrite LgV// ex6_res0; move => yl'. have x1Fj': inc x1' (Vg (isE ex6_F) j') by simpl; rewrite LgV//; rewrite ex6_res0. case /inductive_limit_hi: yl'; set i':= Q _; set z':= P _. simpl => iJl'; rewrite LgV// => zE' x1'v. move/(inl_class_eq_bis (S:=ex6_F) jL j'L x1Fj x1Fj') => [j'' []]. simpl; aw => lejj'' lej'j''; rewrite !LgV//. move: (arg2_sr lejj''); rewrite HLs => jL''. rewrite !ex6_gij_prop1 /x1 x1'v (ex6_prop6b lejj''). rewrite - (ex6_prop6a j'L) (ex6_prop6b lej'j''). move:(HJm lejj'' iJl) (HJm lej'j'' iJl') => ijL'' i'jL''. have zEj'':inc z (Vg (isE (ex6_systemi j'')) i). by rewrite(proj31 (ex6_prop5a jL'')) /=;rewrite LgV//. have zE'j'':inc z' (Vg (isE (ex6_systemi j'')) i'). by rewrite(proj31 (ex6_prop5a jL'')) /=; rewrite LgV//. have zEj''a :inc z (Vg (isE (inl_restr (ex6_prop4 jL''))) i) by simpl;rewrite LgV//. have zE'j''a: inc z' (Vg (isE (inl_restr (ex6_prop4 jL''))) i') by simpl;rewrite !LgV//. have iI': inc i' (isI S). rewrite - ex6_prop3 - HJI; apply/setUb_P; rewrite HJd; ex_tac. rewrite (inl_restr_cf_ev _ iJl zEj'') (inl_restr_cf_ev _ iJl' zE'j''). rewrite(ex6_prop6a jL''). move /(inl_class_eq_bis (S:=(inl_restr (ex6_prop4 jL''))) ijL'' i'jL'' zEj''a zE'j''a ). move => [i'' []]; simpl; aw; move => ha hb; rewrite ! LgV// => eq1. apply/(inl_class_eq_bis iI iI' zE zE'); exists i'';aw. split; [apply:(iorder_gle1 ha) | apply:(iorder_gle1 hb) | done]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)