specialize p (Int.toNat q)
case inl
a b c : ℤθ
q : ℤ
p :
  ∀ (k : ℕ),
    ((↑(unit ^ (3 * ↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * ↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑k))).h % 3 = 0) ∧
      (↑(unit ^ (3 * -↑k))).f % 3 = 1 ∧ (↑(unit ^ (3 * -↑k))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑k))).h % 3 = 0
h1 : 0 < q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
case inl
a b c : ℤθ
q : ℤ
h1 : 0 < q
p :
  ((↑(unit ^ (3 * ↑(Int.toNat q)))).f % 3 = 1 ∧
      (↑(unit ^ (3 * ↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat q)))).h % 3 = 0) ∧
    (↑(unit ^ (3 * -↑(Int.toNat q)))).f % 3 = 1 ∧
      (↑(unit ^ (3 * -↑(Int.toNat q)))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat q)))).h % 3 = 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0