rw [Int.ofNat_one]
case left
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ -((↑n + ↑1) * a.z) = -((↑n + 1) * a.z)

case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ Int.negSucc n * a.w = -((↑n + 1) * a.w)
case right
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ Int.negSucc n * a.w = -((↑n + 1) * a.w)