rw [ge_iff_le]
case inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w1 : 0 < n
⊢ n ≥ 0

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w2 : n ≤ 0
⊢ n ≥ 0 ∨ n < 0
case inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
w1 : 0 < n
⊢ 0 ≤ n

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
w2 : n ≤ 0
⊢ n ≥ 0 ∨ n < 0