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