case inl
o : Ordinal
ho : o ≠ 0
⊢ 0 < o / 0 ^ log 0 o

case inr
b o : Ordinal
ho : o ≠ 0
hb : 0 < b
⊢ 0 < o / b ^ log b o
b o : Ordinal
ho : o ≠ 0
⊢ 0 < o / b ^ log b o
rcases eq_zero_or_pos b with (rfl | hb)
no goals
case inl
o : Ordinal
ho : o ≠ 0
⊢ 0 < o / 0 ^ log 0 o
simpa using Ordinal.pos_iff_ne_zero.2 ho
case inr
b o : Ordinal
ho : o ≠ 0
hb : 0 < b
⊢ b ^ log b o ≤ o
case inr
b o : Ordinal
ho : o ≠ 0
hb : 0 < b
⊢ 0 < o / b ^ log b o
rw [div_pos (opow_ne_zero _ hb.ne')]
no goals
case inr
b o : Ordinal
ho : o ≠ 0
hb : 0 < b
⊢ b ^ log b o ≤ o
exact opow_log_le_self b ho