Theorem: MyNat.succ_add (TheoremProvingLean/inductive_types.lean)

State before:
m k : Nat
⊢ succ k + m = succ (k + m)
Tactic:
induction m with
| zero => rfl
| succ l ih =>
  rw [add_succ, add_succ, ih]
State after:
no goals

State before:
case zero
k : Nat
⊢ succ k + zero = succ (k + zero)
Tactic:
rfl
State after:
no goals

State before:
case succ
k l : Nat
ih : succ k + l = succ (k + l)
⊢ succ k + succ l = succ (k + succ l)
Tactic:
rw [add_succ, add_succ, ih]
State after:
no goals