proposition: Lemma ord_epsilon_p12 x: ordinalp x -> (\2o ^o x = x) -> critical_ordinal \2o opow x.
proof: Proof. move => ox ex; case: (ord_epsilon_p11 ox ex); last by apply: ord_epsilon_p10. move: (oleR OS_omega) olt_2omega => ha hn. by move ->; split => // a a2 au; apply: opow_int_omega. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)