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

State before:
t a b : Nat
⊢ t + a = t + b → a = b
Tactic:
rw [add_comm t a, add_comm t b]
State after:
t a b : Nat
⊢ a + t = b + t → a = b

State before:
t a b : Nat
⊢ a + t = b + t → a = b
Tactic:
exact add_right_cancel
State after:
no goals