proposition: Lemma omega_log_p1 x: \0o <o x -> exists y, [/\ ordinalp y, oopow y <=o x & x <o oopow (osucc y)].
proof: Proof. move => ox. have x1: \1o <=o x by apply/oge1P. have o2:= ole_2omega. move: ord_pow_axioms => [[ax1 _ _ _ ] _ _ _]. move: (ord_induction_p12 (erefl opow') ax1 o2 x1) => [y []]. rewrite - (opow2x _ o2) -(opow2x _ o2) => sa sb sc. by have oy:=(proj31 sa); exists y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)