proposition: Lemma many_der_ex C (E := cnext C) f (g:= many_der f E) (ii:= fun i => (intersectionf i (fun z => fixpoints (Vf g z)))): infinite_c C -> normal_function f E E -> [/\ function g, source g = E, Vf g \0o = f, (forall i, inc i E -> i <> \0o -> Vf g i = ordinalsE E (ii i)) & [/\ forall i, inc i E -> i <> \0o -> lf_axiom (ordinals (fun x y => [/\ inc x (ii i), inc y (ii i) & x <=o y])) E E, (forall i, inc i E -> i <> \0o -> iclosed_set (ii i) /\ ord_cofinal (ii i) E), (forall i, inc i E -> normal_function (Vf g i) E E) & (forall i, inc i E -> i <> \0o -> Imf (Vf g i) = (ii i))]].
proof: Proof. move => pa pb. have oe: ordinalp E by move:(cnext_pr1 (proj1 pa)) => [[]]. case:(transfinite_defined_pr (many_der_aux f E) (ordinal_o_wor oe)). rewrite -/(many_der _ _) -/g ordinal_o_sr => sa sb sc. have ze:= (cnext_leomega pa (proj1 olt_0omega)). have fg: function g by fct_tac. move: (sc _ ze). rewrite /many_der_aux /restriction1; aw. have -> :(segment (ordinal_o E) \0o = \0o) by rewrite ordinal_segment. Ytac0 => pc. pose fpi i := fixpoints (Vf g i). have pd: forall i, inc i E -> i <> \0o -> Vf g i = ordinalsE E (ii i). move => i ie inz; move: (sc _ ie). rewrite /many_der_aux {1 2} /restriction1; aw. have -> :(segment (ordinal_o E) i = i) by rewrite ordinal_segment. Ytac0 ; move => ->; congr (fun z => ordinalsE E z); apply: setIf_exten. move => k ki /=; rewrite restriction1_V // sb. apply: (ordinal_transitive oe ie). split => //. pose pp k := iclosed_set (fpi k)/\ ord_cofinal (fpi k) E /\ forall l, l <o k -> sub (fpi k) (fpi l). have pe: forall i, inc i E -> i<> \0o -> (forall k, k <o i -> pp k) -> iclosed_set (ii i) /\ ord_cofinal (ii i) E. move => i ie inz H. set S := Lg i fpi. have qa: fgraph S by rewrite /S; fprops. have qb: domain S = i by rewrite /S; aw. move /(cnextP (proj1 pa)): ie => [u1 u2]. have qc: ordinalp (domain S) by rewrite qb. have qd: cardinal (domain S) <=c C by rewrite qb. have qe: nonempty (domain S). by exists \0c;move:(olt_i (ord_ne0_pos u1 inz)); rewrite - qb. have qf:(intersectionb S) = ii i. rewrite /ii /S /fpi /intersectionb Lgd;apply:setIf_exten => k kd. by rewrite LgV. move:( closed_cofinal_inter pa qa qc qd qe); rewrite -/E qf qb; apply. + by move => k ki; rewrite /S LgV//; move /(oltP u1): ki => /H /proj1. + by move => k ki;rewrite /S LgV//; move /(oltP u1): ki => /H /proj2/proj1. + move => k j kj ki ji; rewrite /S !LgV//. by move /(oltP u1): ji => /H /proj2/proj2; apply. have pf: forall i, inc i E -> i <> \0o -> iclosed_set (ii i) /\ ord_cofinal (ii i) E -> normal_function (Vf g i) E E /\ Imf (Vf g i) = ii i. move => i ie inz [ta tb]; move: (ordinals_set_normal1 pa ta tb). by have -> //: ordinalsE E (ii i) = Vf g i; rewrite pd => //; move => [_]. have pg: forall k, inc k E -> pp k. move =>k ke. have ok:= Os_ordinal oe ke. move: k ok ke; apply:least_ordinal2 => l ol etc le. have ss: forall i, inc i E -> (source (Vf g i)) = E. move => i ie; case: (equal_or_not i \0o) => iz. by rewrite iz pc; move: pb => [[]]. by rewrite (pd i ie iz) /ordinalsE; aw. case: (equal_or_not l \0o) => l0. have sfe: source f = E by move: pb => [ [] ]. rewrite l0 /pp/fpi pc; split. apply:(iclosed_fixpoints_fun oe) => //; rewrite sfe. split; last by move => m /olt0. by apply: normal_fix_cofinal. have ww: forall k, k <o l -> pp k. move /(oltP oe): le => lte. move => t tl; apply: etc => //;apply/(oltP oe); exact:(olt_ltT tl lte). move: (pe _ le l0 ww) => r0; move: (pf l le l0 r0) => [ta tb]. have tc: iclosed_set (fpi l). by move: (iclosed_fixpoints_fun oe ta); rewrite /fpi/fixpoints ss. have td: ord_cofinal (fpi l) E by rewrite /fpi; apply: normal_fix_cofinal. split => //; split => //. move => m lm t. have lle : l <o E by apply /oltP. have me:=(olt_i(olt_ltT lm lle)). rewrite /fpi /fixpoints ss // ss //. move => /Zo_P [ua ub]; apply /Zo_P; split => //. have fv: function (Vf g l) by move: ta => [[]]. have ti: inc t (ii l). rewrite - tb; apply /(Imf_P fv); rewrite ss//; exists t => //. by move:(setIf_hi ti (olt_i lm)) => /Zo_P []. have ph: forall i, inc i E -> i <> \0o -> normal_function (Vf g i) E E /\ Imf (Vf g i) = ii i. move => i ie inz; apply: pf => //; apply: pe => // k ke; apply: pg. have iE: i <o E by apply/oltP. exact:(olt_i(olt_ltT ke iE)). split. + move => i ie inz. have [ta tb]:iclosed_set (ii i) /\ ord_cofinal (ii i) E. apply: pe => // k ke;apply: pg. have iE: i <o E by apply/oltP. apply /oltP => //; exact:(olt_ltT ke iE). move: (proj1 (ordinals_set_iso (proj1 ta))). by rewrite (ord_cofinal_p5 pa) -/E // => h t ti; apply: (proj1 tb); apply: h. + move => i ide inz; apply: pe => // k ki; apply: pg. have iE: i <o E by apply/oltP. apply /oltP => //; exact:(olt_ltT ki iE). + move => i ide; case (equal_or_not i \0o);first by move => ->; ue. move => inz; exact: (proj1 (ph i ide inz)). + move => i ide inz;exact: (proj2 (ph i ide inz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)