simp at t
case inl.inl.h
a b c : ℤθ
n : ℤ
h : n ≠ 0
p3 : 0 = n
t : n = 0 ∧ n ≠ 0
⊢ False

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
⊢ ∃ 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))