2 goals
case nat.zero
b : ℕ
⊢ 0 + b = b + 0

case nat.succ
b a : ℕ
⊢ nat.succ a + b = b + nat.succ a
induction_naming.lean:1:0: warning: declaration '[anonymous]' uses sorry
2 goals
case nat.zero
b : ℕ
⊢ 0 + b = b + 0

case nat.succ
b a_n : ℕ,
a_ih : a_n + b = b + a_n
⊢ nat.succ a_n + b = b + nat.succ a_n
induction_naming.lean:8:0: warning: declaration '[anonymous]' uses sorry
2 goals
case nat.zero
b : ℕ
⊢ 0 + b = b + 0

case nat.succ
b n : ℕ,
ih : n + b = b + n
⊢ nat.succ n + b = b + nat.succ n
induction_naming.lean:17:0: warning: declaration '[anonymous]' uses sorry
