constructor
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 right.left
a✝ b c : ℤθ
n : ℕ
a : ℤθ
⊢ Int.negSucc n * a.g = -((↑n + 1) * a.g)

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