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

State before:
m : Nat
⊢ zero + zero = zero
Tactic:
rfl
State after:
no goals

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