proposition: Lemma ord_epsilon_p10 x: epsilonp x -> critical_ordinal \2o opow x.
proof: Proof. move=> oex;move: (oex) => [ox _]; move: (ord_eps_p3 oex) => xo. split => //. exact: (proj1 xo). exact: (olt_ltT olt_2omega xo). move=> a a2 ax; move: (ord_epsilon_p9 oex ax) => [_ _ p]; apply: (p a2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)