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

case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.g = -((↑n + 1) * a.g) ∧ Int.negSucc n * a.h = -((↑n + 1) * a.h)
case left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ -(↑(n + 1) * a.f) = -((↑n + 1) * a.f)

case right
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.g = -((↑n + 1) * a.g) ∧ Int.negSucc n * a.h = -((↑n + 1) * a.h)