case zero

⊢ ↑toOrdinal ↑Nat.zero = ↑Nat.zero

case succ
n : ℕ
hn : ↑toOrdinal ↑n = ↑n
⊢ ↑toOrdinal ↑(Nat.succ n) = ↑(Nat.succ n)
n : ℕ
⊢ ↑toOrdinal ↑n = ↑n
induction' n with n hn
no goals
case zero

⊢ ↑toOrdinal ↑Nat.zero = ↑Nat.zero
rfl
case succ
n : ℕ
hn : ↑toOrdinal ↑n = ↑n
⊢ nadd (↑toOrdinal ↑n) 1 = ↑n + 1
case succ
n : ℕ
hn : ↑toOrdinal ↑n = ↑n
⊢ ↑toOrdinal ↑(Nat.succ n) = ↑(Nat.succ n)
change nadd (toOrdinal n) 1 = n + 1
case succ
n : ℕ
hn : ↑toOrdinal ↑n = ↑n
⊢ nadd (↑n) 1 = ↑n + 1
case succ
n : ℕ
hn : ↑toOrdinal ↑n = ↑n
⊢ nadd (↑toOrdinal ↑n) 1 = ↑n + 1
rw [hn]
no goals
case succ
n : ℕ
hn : ↑toOrdinal ↑n = ↑n
⊢ nadd (↑n) 1 = ↑n + 1
apply nadd_one