case zero

⊢ ack 1 zero = zero + 2

case succ
n : ℕ
IH : ack 1 n = n + 2
⊢ ack 1 (succ n) = succ n + 2
n : ℕ
⊢ ack 1 n = n + 2
induction' n with n IH
no goals
case zero

⊢ ack 1 zero = zero + 2
rfl
no goals
case succ
n : ℕ
IH : ack 1 n = n + 2
⊢ ack 1 (succ n) = succ n + 2
simp [IH]