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

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

State before:
case zero

⊢ zero + zero = zero
Tactic:
rfl
State after:
no goals

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