have h := lt_or_le 0 q
a b c : ℤθ
q : ℤ
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0
a b c : ℤθ
q : ℤ
h : 0 < q ∨ q ≤ 0
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0