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

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