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

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