induction' k with b hb
case right
a b c : ℤθ
k : ℕ
⊢ (↑(unit ^ (3 * -↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑k))).h % 3 = 0
case right.zero
a b c : ℤθ
⊢ (↑(unit ^ (3 * -↑Nat.zero))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑Nat.zero))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑Nat.zero))).h % 3 = 0

case right.succ
a b✝ c : ℤθ
b : ℕ
hb : (↑(unit ^ (3 * -↑b))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑b))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑b))).h % 3 = 0
⊢ (↑(unit ^ (3 * -↑(Nat.succ b)))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Nat.succ b)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Nat.succ b)))).h % 3 = 0