b o : Ordinal
hb : 1 < b
⊢ o < b ^ succ (log b o)
b o : Ordinal
hb : 1 < b
⊢ o / b ^ log b o < b
rw [div_lt (opow_pos _ (zero_lt_one.trans hb)).ne', ← opow_succ]
no goals
b o : Ordinal
hb : 1 < b
⊢ o < b ^ succ (log b o)
exact lt_opow_succ_log_self hb o