simp at q
case intro.inr
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
p : ℕ
q : 3 ^ (n + 1) > 3 ^ (n + 1) * p
hp : 3 * n = 3 ^ (n + 1) * p
ss : 0 < p
⊢ False
case intro.inr
a b c : ℤθ
n : ℕ
j : 1 ≤ n
s : ∀ (x : ℕ), ¬3 ^ x ∣ 3 * n ∧ ¬3 ^ (x + 1) ∣ 3 * n ∨ 3 ^ x ∣ 3 * n ∧ 3 ^ (x + 1) ∣ 3 * n
p : ℕ
hp : 3 * n = 3 ^ (n + 1) * p
ss : 0 < p
q : p = 0
⊢ False