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 < ω
dsimp only
a b : Ordinal
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ ↑(m * n) < ω
a b : Ordinal
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ ↑m * ↑n < ω
rw [← nat_cast_mul]
no goals
a b : Ordinal
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ ↑(m * n) < ω
apply nat_lt_omega