change
  (⟨Int.negSucc n * a.f, Int.negSucc n * a.g, Int.negSucc n * a.h⟩ : ℤθ) =
    (⟨-(Int.ofNat n.succ * a.f), -(Int.ofNat n.succ * a.g), -(Int.ofNat n.succ * a.h)⟩ : ℤθ)
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ zsmul (Int.negSucc n) a = neg (zsmul (↑n + 1) a)
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ { f := Int.negSucc n * a.f, g := Int.negSucc n * a.g, h := Int.negSucc n * a.h } =
    { f := -(Int.ofNat (Nat.succ n) * a.f), g := -(Int.ofNat (Nat.succ n) * a.g), h := -(Int.ofNat (Nat.succ n) * a.h) }