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

State before:
m n : Nat
⊢ m ≠ zero → pred m + n = pred (m + n)
Tactic:
intro hm
State after:
m n : Nat
hm : m ≠ zero
⊢ pred m + n = pred (m + n)

State before:
m n : Nat
hm : m ≠ zero
⊢ pred m + n = pred (m + n)
Tactic:
rw [add_comm (pred m) n, add_pred n m hm, add_comm]
State after:
no goals