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

case inr
b o : Ordinal
ho : o ≠ 0
hb : b ≠ 0
⊢ o % b ^ log b o < o
b o : Ordinal
ho : o ≠ 0
⊢ o % b ^ log b o < o
rcases eq_or_ne b 0 with (rfl | hb)
no goals
case inl
o : Ordinal
ho : o ≠ 0
⊢ o % 0 ^ log 0 o < o
simpa using Ordinal.pos_iff_ne_zero.2 ho
no goals
case inr
b o : Ordinal
ho : o ≠ 0
hb : b ≠ 0
⊢ o % b ^ log b o < o
exact (mod_lt _ <| opow_ne_zero _ hb).trans_le (opow_log_le_self _ ho)