proposition: Lemma pow_fix_enumeration1 a: \2o <=o a -> a <o omega0 -> forall x, ordinalp x -> first_derivation (opow a) x = Yo (x = \0o) omega0 (epsilon_fam (x -o \1o)).
proof: Proof. move => age2 ao. have npa:= (opow_normal age2). have npb:= oopow_normal. have pa := (iclosed_fixpoints npa). have na :=(ordinals_col_p2 pa). have oa:= proj31_1 ao. move: OS_omega => oo. have aux: forall x, ordinalp x -> a ^o x = x -> x = omega0 \/ epsilonp x. move => x ox h; apply: (ord_epsilon_p11 ox). move: (proj1 (ord_epsilon_p13 oa ox h)) => h1; case: (h1 ao); last by exact. by move=> [a1 _]; case :(oltNge olt_12); rewrite - a1. have aux1 : forall x, ordinalp x -> a ^o x = x -> omega0 <=o x. move => x ox xv; case: (aux _ ox xv); first by move => ->; apply:(oleR oo). by move /ord_eps_p3 => []. have aux2: forall x, ordinalp x -> oopow x = x -> a ^o x = x. move => x ox oox; move: (conj ox oox) => xox. have ax:= (olt_leT ao (proj1 (ord_eps_p3 xox))). by apply: (proj33 (ord_epsilon_p9 xox ax)). have npc:=(first_derivation_p0 npa). have sd0:(first_derivation (opow a) \0o) = omega0. rewrite (first_derivation_p1 npa). move: (normal_ofs_fix npa OS0) => [sa sb sc]; apply: oleA. exact: (sc _ (ole0x oo) (opow_int_omega age2 ao)). exact: (aux1 _ (proj32 sa) sb). apply:(normal_ofs_uniqueness (p:= fun z => (epsilon_fct (osucc z)))). - exact: npc. - have aa: forall x,ordinalp x -> omega0 <o epsilon_fam x. by move => x /epsilon_fam_pr0 /ord_eps_p3. move:epsilon_fam_pr5 => [sa sb]. split. move => u v uv /=. case: (equal_or_not v \0o) => vnz; first by case: (@olt0 u); ue. Ytac0;Ytac uz; first by apply: aa;apply: (OS_diff OS1 (proj32_1 uv)). apply: sa; apply:oprec_Mlt => //; exact:(ord_ne0_pos (proj31_1 uv) uz). move => x lx; move: (limit_nz lx) => xnz; Ytac0. move: (lx) => [ox zix lxx]. rewrite (odiff_1inf (limit_ge_omega lx)) (sb _ lx). have oe: forall z, inc z x -> ordinalp (epsilon_fam (z -o \1o)). move=> z /(Os_ordinal ox) h;apply: (ofs_sincr sa); apply: (OS_diff OS1 h). apply: ord_sup_1cofinal; first split. * move => s /funI_P [z zx ->]; apply /funI_P. have oz:= Os_ordinal ox zx. case: (oleT_el OS_omega oz) => czo. exists z => //; rewrite (odiff_1inf czo); Ytac zz; last by exact. by case: (oltNge olt_0omega); rewrite - zz. exists (osucc z); first by apply: lxx. move: (@osucc_nz z) => zz; Ytac0; case: (ozero_dichot oz) => zz1. by rewrite zz1 osucc_zero (odiff_wrong (oleR OS1)). by rewrite (oprec_nat2 zz1 czo) - (oprec_nat zz1 czo). * move => s /funI_P [z zx ->]; Ytac zp. exists (epsilon_fam \0o); first by apply/funI_P; ex_tac; ue. exact: (proj1 (aa _ OS0)). move: (oleR (oe _ zx)) => l1. have ssx: inc (z -o \1o) x. move: (odiff_Mle OS1 (Os_ordinal ox zx)) => h1. by move/(oltP ox): zx => h;apply/(oltP ox); apply: (ole_ltT h1 h). exists (epsilon_fam (z -o \1o)) => //; apply/funI_P; ex_tac. * move => s /funI_P [z za ->]; Ytac zz;[ exact | by apply: oe]. - move => x ox; rewrite (first_derivation_p3 npa ox) /epsilon_fct. move: (sincr_incr (proj1 npc) (ole0x ox)); rewrite sd0. move /oltSleP; set t := osucc _ => oot. have ot:= proj32_1 oot. move: (normal_ofs_fix npa ot) (normal_ofs_fix npb ot). move => [sa sb sc][sd se sf]; apply: oleA. apply: (sc _ sd); apply: (aux2 _ (proj32 sd) se). apply: (sf _ sa) ; case: (aux _ (proj32 sa) sb); last by move => []. move => e1; rewrite e1 in sa; case:(oltNge oot sa). - move => x ox; move: (@osucc_nz x)=> snz; Ytac0. case: (oleT_el oo ox) => cox. rewrite (odiff_1inf cox). rewrite (odiff_1inf (oleT cox (proj1(oltS ox)))). Ytac xz; first by move: olt_0omega; rewrite - xz => /(oleNgt cox). by apply:epsilon_fam_pr4. case: (ozero_dichot ox) => xz. Ytac0; rewrite xz osucc_zero (odiff_wrong (oleR OS1)). apply: epsilon_fam_pr2''. move: (xz) => [_ xnz]; Ytac0; rewrite (oprec_nat2 xz cox). by apply: epsilon_fam_pr4; apply: (OS_diff OS1 ox). - Ytac0; exact sd0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)