no goals
m : Nat
⊢ 0 + m = 0 → 0 = 0
simp [Nat.zero_add]
n m : Nat
h : succ (n + m) = 0
⊢ n + 1 = 0
n m : Nat
h : n + 1 + m = 0
⊢ n + 1 = 0
rw [add_one, succ_add] at h
no goals
n m : Nat
h : succ (n + m) = 0
⊢ n + 1 = 0
cases succ_ne_zero _ h