proposition: Lemma prl_ne1_res5: (exists2 A, countable_set A & cofinal(psr S) A ) -> forall i, inc i (psI S) -> surjection (prl_can_fun S i).
proof: Proof. move => [A countA cfA]. case:(countable_finite_or_N countA) => cardA. by apply: (prl_ne1_res3 cfA cardA). move: (prl_ne1_res4 cardA cfA) => [f [ff sf fp1 fp2]]. have otr := proj33 (ps_preorder_r S). have fiI i: natp i -> inc (Vf f i) (psI S). by move => iN; move:(arg1_sr (fp1 _ iN)); rewrite ps_substrate_r. have fp3 i j : natp i -> natp j -> i <=c j -> gle (psr S) (Vf f i) (Vf f j). move => iN jN leij. rewrite - (cdiff_pr leij). move:(NS_diff i jN); move:(j -c i). clear jN leij; apply:Nat_induction. rewrite (csum0r (CS_nat iN)); apply: (proj32 (ps_preorder_r S)). rewrite ps_substrate_r; apply:(fiI _ iN). move => n nN hr; rewrite (csum_nS _ nN). exact: (otr _ _ _ hr (fp1 _ (NS_sum iN nN))). move => i iI; move: (fp2 _ iI) => [n nN ha]. apply:(prl_ne1_surj_rec ha) ; clear i iI ha. move:(prl_can_fun_fp (fiI _ nN)); set fn := (prl_can_fun S (Vf f n)). move=> [fbf sfn tfn]; split => //; rewrite sfn tfn => [y yIEn]. pose nexty i y z := inc z (Vg (psE S) (Vf f (csucc (n +c i)))) /\ Vf (Vg (psf S) (J (Vf f (n +c i)) (Vf f (csucc (n +c i))))) z = y. pose ch2 i y := choose (nexty i y). have pa i t: natp i -> inc t (Vg (psE S) (Vf f (n +c i))) -> nexty i t (ch2 i t). move => iN tE. move:(fp1 _ (NS_sum nN iN)) => le1. move: (sjf le1) (ps_function_f le1) => [fg sg][_ sog tag]. move: sg; rewrite sog tag; aw => h; move:(h t tE) => [x xa xb]. by apply: choose_pr; exists x. move:(induction_defined_pr0(fun n v => ch2 n v) y). set g := induction_defined0 _ _; move => [sg [fg _] g0 gS]. have np0 := (csum0r (CS_nat nN)). have pb i: natp i -> inc (Vf g i) (Vg (psE S) (Vf f (n +c i))). move: i;apply: Nat_induction; first by rewrite np0 g0. move => i iN hr. rewrite (gS _ iN); rewrite (csum_nS _ iN); exact:(proj1 (pa _ _ iN hr)). have pc i: natp i -> Vf (Vg (psf S) (J (Vf f (n +c i)) (Vf f (csucc (n +c i))))) (Vf g (csucc i)) = Vf g i. move => iN; rewrite (gS _ iN); exact:(proj2 (pa _ _ iN (pb _ iN))). pose pp3 j i := natp i /\ gle (psr S) j (Vf f (n +c i)). pose ch3 j := choose (pp3 j). have ch3p i: inc i (psI S) -> pp3 i (ch3 i). move => iI; rewrite /ch3;apply: choose_pr. move: (fp2 _ iI) => [j jN] leab; case: (NleT_ee jN nN) => lea. exists \0c; split; fprops; rewrite np0. exact:(otr _ _ _ leab (fp3 _ _ jN nN lea)). move:(cdiff_pr lea) => leb; exists (j -c n); split => //; fprops; ue. pose xi i := Vf (Vg (psf S) (J i (Vf f (n +c (ch3 i))))) (Vf g (ch3 i)). have xiEi i: inc i (psI S) -> inc (xi i) (Vg (psE S) i). move => iI. move: (ch3p _ iI) => [qa qb]. move:(ps_function_f qb); rewrite /xi; aw; set mf := (Vg (psf S) _). by move => [fm sm tm]; Wtac; rewrite sm; apply: pb. have Ha p k : natp k -> p <=c k -> Vf g p = Vf (Vg (psf S) (J (Vf f (n +c p)) (Vf f (n +c k)))) (Vf g k). move => kN lpk; move: (NS_le_nat lpk kN) => pN. rewrite - (cdiff_pr lpk); move:(NS_diff p kN); move:(k -c p). clear k kN lpk; apply:Nat_induction. have qq:inc (Vf f (n +c p)) (psI S) by apply: (fiI _ (NS_sum nN pN)). by rewrite (csum0r (CS_nat pN)) (prl_prop5 qq (pb _ pN)). move=> k kN h; move: (NS_sum pN kN) => pkN. rewrite (csum_nS _ kN) (gS _ pkN) h (csum_nS _ pkN). move: (pa _ _ pkN (pb _ pkN)) => []; set u := ch2 _ _ => uE <-. apply:prl_prop3 uE. by apply: fp3; fprops; rewrite csumA; apply:csum_M0le; fprops. by apply: fp3; fprops. have Hb i k p: natp k -> p <=c k -> gle (psr S) i (Vf f (n +c p)) -> Vf (Vg (psf S) (J i (Vf f (n +c p)))) (Vf g p) = Vf (Vg (psf S) (J i (Vf f (n +c k)))) (Vf g k). move => kN lpk lei1; move: (NS_le_nat lpk kN) => pN. have le2: gle (psr S) (Vf f (n +c p)) (Vf f (n +c k)). by apply:(fp3 _ _(NS_sum nN pN) (NS_sum nN kN)); apply:csum_Meqle. by rewrite - (prl_prop3 lei1 le2 (pb _ kN)) - (Ha _ _ kN lpk). have xii i j: inc i (psI S) -> natp j -> gle (psr S) i (Vf f (n +c j)) -> xi i = Vf (Vg (psf S) (J i (Vf f (n +c j)))) (Vf g j). move => iI jN ha. move: (ch3p _ iI) => [qa qb]; rewrite /xi. set k := cmax j (ch3 i). move: (Nmax_p1 jN qa);rewrite -/k; move => [kN kl1 kl2]. by rewrite (Hb _ _ _ kN kl1 ha) (Hb _ _ _ kN kl2 qb). pose x := Lg (psI S) xi. suff: inc x (projective_limit S). move => xl; exists x => //; move : (fiI _ nN) => ha. rewrite (prl_proj_ev ha xl) /x LgV//. have ll: gle (psr S) (Vf f n) (Vf f n). by apply: (proj32 (ps_preorder_r S)); rewrite ps_substrate_r;apply: fiI. move:(xii _ _ ha NS0); rewrite np0 => h. by rewrite (h ll) (prl_prop5 ha) => //; move: (pb _ NS0); rewrite np0. rewrite /x;apply/prl_limitP; split. - fprops. - by aw. - move => i iI; rewrite LgV//; apply:(xiEi _ iI). - move => i j leij. move:(prl_prop0 leij) => [iI jI]. move: (ch3p _ jI) => [chN lejc]. have leic:= (otr _ _ _ leij lejc). by rewrite !LgV // (xii _ _ iI chN leic) (prl_prop3 leij lejc) //; apply: pb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)