have w :
  ((unit ^ ((3 : ℤ) * -(b + 1 : ℤ)) : ℤθˣ) : ℤθ) =
    ((unit ^ (3 * -(b : ℤ)) : ℤθˣ) : ℤθ) * ((unit ^ (-3 : ℤ) : ℤθˣ) : ℤθ) :=
  by
  rw [neg_add, mul_add, mul_neg_one, zpow_add]
  norm_cast
case right.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0
case right.succ.intro.intro
a b✝ c : ℤθ
b : ℕ
h1 : (↑(unit ^ (3 * -↑b))).f % 3 = 1
h2 : (↑(unit ^ (3 * -↑b))).g % 3 = 0
h3 : (↑(unit ^ (3 * -↑b))).h % 3 = 0
p : Nat.succ b = b + 1
w : ↑(unit ^ (3 * -(↑b + 1))) = ↑(unit ^ (3 * -↑b)) * ↑(unit ^ (-3))
⊢ (↑(unit ^ (3 * -↑(b + 1)))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑(b + 1)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(b + 1)))).h % 3 = 0