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

State before:
a b : Nat
⊢ a + b = a → b = 0
Tactic:
intro h
State after:
a b : Nat
h : a + b = a
⊢ b = 0

State before:
a b : Nat
h : a + b = a
⊢ b = 0
Tactic:
rw [← add_zero a] at h
State after:
a b : Nat
h : a + zero + b = a + zero
⊢ b = 0

State before:
a b : Nat
h : a + zero + b = a + zero
⊢ b = 0
Tactic:
exact (add_left_cancel _ _ _ h)
State after:
no goals