have r := neg_le_neg h2
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 :
  (↑(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
case inr.intro
a b c : ℤθ
q : ℤ
h2 : q ≤ 0
p1 :
  (↑(unit ^ (3 * ↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * ↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * ↑(Int.toNat (-q))))).h % 3 = 0
p2 :
  (↑(unit ^ (3 * -↑(Int.toNat (-q))))).f % 3 = 1 ∧
    (↑(unit ^ (3 * -↑(Int.toNat (-q))))).g % 3 = 0 ∧ (↑(unit ^ (3 * -↑(Int.toNat (-q))))).h % 3 = 0
r : -0 ≤ -q
⊢ (↑(unit ^ (3 * q))).f % 3 = 1 ∧ (↑(unit ^ (3 * q))).g % 3 = 0 ∧ (↑(unit ^ (3 * q))).h % 3 = 0