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

State before:
a b : Nat
h : a + b = zero
⊢ b = zero
Tactic:
cases b with
| zero => rfl
| succ d =>
  rw [add_succ] at h
  contradiction
State after:
no goals

State before:
case zero
a : Nat
h : a + zero = zero
⊢ zero = zero
Tactic:
rfl
State after:
no goals

State before:
case succ
a d : Nat
h : a + succ d = zero
⊢ succ d = zero
Tactic:
rw [add_succ] at h
State after:
case succ
a d : Nat
h : succ (a + d) = zero
⊢ succ d = zero

State before:
case succ
a d : Nat
h : succ (a + d) = zero
⊢ succ d = zero
Tactic:
contradiction
State after:
no goals