proposition: Lemma pow_fix_enumeration2 a (b := inverse_epsilon (epsilon_fct (osucc a))): omega0 <=o a -> forall x, ordinalp x -> first_derivation (opow a) x = (epsilon_fam (b +o x)).
proof: Proof. move => ao. have age2:= (oleT ole_2omega ao). move: (least_critical_pow ao); rewrite -/b; move => bp. have oa:=proj32 ao. move:(inverse_epsilon_pr (epsilon_fct_pr1 (OS_succ oa))). rewrite -/b; move => [ob eb]. have npa:= (opow_normal age2). have npb:= oopow_normal. have npc:= (first_derivation_p0 npa). move:(ordinals_col_p2 (iclosed_fixpoints npa)) => na. move: OS_omega => oo. have aux2: forall x, a <o x -> omega0 ^o x = x -> a ^o x = x. move => x ax oox; move: (conj (proj32 (proj1 ax)) oox) => xox. by move:(ord_epsilon_p9 xox ax) => [_ _]; apply. have aux0: the_least_fixedpoint_ge [eta opow a] \0o = epsilon_fam b. move: (normal_ofs_fix npa OS0) => [sa sb sc]. move: bp => [sa' sb' sc']. apply: oleA; [by apply:sc | by apply:sc']. apply:(normal_ofs_uniqueness (p:= fun z => (epsilon_fct (osucc z)))). - exact: npc. - exact: (normal_ofs_compose epsilon_fam_pr5 (osum_normal ob)). - move => x ox; rewrite (first_derivation_p3 npa ox) /epsilon_fct. have hh:= (ole0x ox). move: (sincr_incr (proj1 npc) hh) => /oltSleP. rewrite (first_derivation_p1 npa) aux0. set t := osucc _; rewrite eb => sa1. move:(epsilon_fct_pr0 (OS_succ oa)); move => [sa2 _ _]. move: (ole_ltT sa2 sa1) => [] /oleSltP lat _. have ot:=proj32_1 lat. 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 _ _ se); apply:(olt_leT lat sd). apply: (sf _ sa). move: (ord_epsilon_p13 oa (proj32 sa) sb) => [_ h1]. move: (h1 ao) => [[_ h2] _]; exact h2. - move => x ox; rewrite - (osum2_succ ob ox); apply: epsilon_fam_pr4; fprops. - rewrite (osum0r ob) - aux0 (first_derivation_p1 npa); reflexivity. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)