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

State before:
d : Nat
⊢ d + one = succ d
Tactic:
rw [succ_eq_add_one]
State after:
no goals