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

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

State before:
a b : Nat
h : b + a = zero
⊢ a = zero
Tactic:
apply add_left_eq_zero h
State after:
no goals