case zero

⊢ ack 2 zero = 2 * zero + 3

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

⊢ ack 2 zero = 2 * zero + 3
rfl
no goals
case succ
n : ℕ
IH : ack 2 n = 2 * n + 3
⊢ ack 2 (succ n) = 2 * succ n + 3
simpa [mul_succ]