proposition: Lemma prl_ne1_res4 A: cardinal A = aleph0 -> cofinal (psr S) A -> exists f, [/\ function f, source f = Nat, forall i, natp i -> gle (psr S) (Vf f i) (Vf f (csucc i)) & forall i, inc i (psI S) -> exists2 n, natp n & gle (psr S) i (Vf f n) ].
proof: Proof. move => ha hb. pose pp pr z := gle (psr S) (P pr) z /\ gle (psr S) (Q pr) z. pose ch1 pr := choose (pp pr). have pa pr: inc pr (coarse (substrate (psr S))) -> pp pr (ch1 pr). by move => /setX_P[qa qb qc]; apply: choose_pr; move:(rdr qb qc). have pb i j: inc i (psI S) -> inc j (psI S) -> gle (psr S) i (ch1 (J i j)) /\ gle (psr S) j (ch1 (J i j)). move => qa qb. have: (inc (J i j) (coarse (substrate (psr S)))). by rewrite ps_substrate_r; apply:setXp_i. by move/pa; rewrite /pp; aw. move: (esym ha);rewrite aleph0_pr1 => /card_eqP [g [[[fg _] [_ sjg]] sg tg]]. move:(induction_defined_pr0(fun n v => ch1 (J (Vf g n) v))(Vf g \0c)). set f := induction_defined0 _ _; move => [sf [ff _] f0 fS]. have pc n: natp n -> inc (Vf g n) (psI S). move => nN; move:(proj1 hb); rewrite ps_substrate_r; apply; Wtac; ue. have pd n: natp n -> inc (Vf f n) (psI S). move:n; apply:Nat_induction; first by rewrite f0; apply: pc; fprops. move => n nN hr; rewrite (fS _ nN). by move:(arg2_sr (proj1 (pb _ _ (pc _ nN) hr))); rewrite ps_substrate_r. exists f; split => //. move => i iN; rewrite (fS _ iN);exact:(proj2 (pb _ _ (pc _ iN) (pd _ iN))). move => i iI. have isr:inc i (substrate (psr S)) by rewrite ps_substrate_r. move:(proj2 hb i isr) => [y yA leiy]; rewrite sg tg in sjg. move:(sjg _ yA) => [n nN yv]. move:(arg2_sr leiy); rewrite ps_substrate_r => yI. exists (csucc n); first by apply: (NS_succ nN). move:(proj1 (pb y (Vf f n) yI (pd _ nN))); rewrite (fS _ nN) - yv. apply: (proj33 (ps_preorder_r S) _ _ _ leiy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)