rw [Int.ofNat_zero, neg_zero, MulZeroClass.mul_zero]
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.zero
a b c : ℤθ
⊢ (↑(unit ^ 0)).f % 3 = 1 ∧ (↑(unit ^ 0)).g % 3 = 0 ∧ (↑(unit ^ 0)).h % 3 = 0