rw [Nat.succ_add]
case succ
m n_1 : ℕ
n_ih : ¬n_1 = 0 → n_1 - 1 + m = n_1 + m - 1
h : ¬Nat.succ n_1 = 0
⊢ Nat.succ n_1 - 1 + m = Nat.succ n_1 + m - 1
case succ
m n_1 : ℕ
n_ih : ¬n_1 = 0 → n_1 - 1 + m = n_1 + m - 1
h : ¬Nat.succ n_1 = 0
⊢ Nat.succ n_1 - 1 + m = Nat.succ (n_1 + m) - 1