linarith
case left
a✝ b c : ℤα
n : ℕ
a : ℤα
⊢ (↑n + 1) * a.z = a.z + ↑n * a.z

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