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

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

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