a b : Ordinal
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ ↑(m ^ n) < ω
a b : Ordinal
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ (fun x x_1 => x ^ x_1) ↑m ↑n < ω
simp_rw [← nat_cast_opow]
no goals
a b : Ordinal
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ ↑(m ^ n) < ω
apply nat_lt_omega