case zero
a b c : Ordinal
⊢ a ♯ ↑Nat.zero = a + ↑Nat.zero

case succ
a b c : Ordinal
n : ℕ
hn : a ♯ ↑n = a + ↑n
⊢ a ♯ ↑(Nat.succ n) = a + ↑(Nat.succ n)
a b c : Ordinal
n : ℕ
⊢ a ♯ ↑n = a + ↑n
induction' n with n hn
no goals
case zero
a b c : Ordinal
⊢ a ♯ ↑Nat.zero = a + ↑Nat.zero
simp
no goals
case succ
a b c : Ordinal
n : ℕ
hn : a ♯ ↑n = a + ↑n
⊢ a ♯ ↑(Nat.succ n) = a + ↑(Nat.succ n)
rw [Nat.cast_succ, add_one_eq_succ, nadd_succ, add_succ, hn]