have p : n ≥ 0 ∨ n < 0 := by
  have w := lt_or_le 0 n
  cases' w with w1 w2
  left; rw [ge_iff_le]; rw [le_iff_lt_or_eq]; left; exact w1
  rw [le_iff_lt_or_eq] at w2
  cases' w2 with w3 w4
  right; exact w3
  left; rw [ge_iff_le]; rw [le_iff_lt_or_eq]; right; exact Eq.symm w4
a b c : ℤθ
n : ℤ
h : n ≠ 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
a b c : ℤθ
n : ℤ
h : n ≠ 0
p : n ≥ 0 ∨ n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))