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

State before:
n : Nat
⊢ succ n = n + one
Tactic:
rw [one_eq_succ_zero, add_succ, add_zero]
State after:
no goals