have p5 : 1 ≤ Int.toNat n :=
  by
  have s := Nat.eq_zero_or_pos (Int.toNat n)
  cases' s with s1 s2
  exfalso
  simp at s1
  push_neg at s1
  apply lt_irrefl 0 (lt_of_lt_of_le p4 s1)
exact s2
case inl.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))
case inl.inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p4 : 0 < n
p5 : 1 ≤ Int.toNat n
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))

case inr
a b c : ℤθ
n : ℤ
h : n ≠ 0
p2 : n < 0
⊢ ∃ a b, 1 ≤ a ∧ (3 * n = 3 ^ a * (3 * b + 1) ∨ 3 * n = 3 ^ a * (3 * b + 2))