proposition: Lemma least_critical_pow a (b := inverse_epsilon (epsilon_fct (osucc a))): omega0 <=o a -> least_fixedpoint_ge (opow a) \0o (epsilon_fam b).
proof: Proof. move => ooa. have oa:= (OS_succ (proj32 ooa)). move:(epsilon_fct_pr1 oa) => oeea; move:(oeea) => [ooeea _]. move: (inverse_epsilon_pr oeea); rewrite -/b; move => [ob eb]. move:(epsilon_fct_pr0 oa); rewrite eb; move => [sa sb sc]. have a2:= (oleT (ole_2omega) ooa). split; first by apply:(ole0x ooeea). have lt1: a <o epsilon_fct (osucc a) by apply /oleSltP. by move: (ord_epsilon_p9 oeea lt1)=> [_ _]; apply. move => z zp h; move: (ord_epsilon_p13 (proj32 ooa) (proj32 zp) h) => [_ h1]. by move: (h1 ooa) => [[_ ta] tb]; apply: sc => //; apply /oleSltP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)