clear t
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
t : 3 ^ (n + 1) ∣ 3 * n
q : 3 ^ (n + 1) > 3 * n
⊢ ¬3 ^ (n + 1) ∣ 3 * n
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
q : 3 ^ (n + 1) > 3 * n
⊢ ¬3 ^ (n + 1) ∣ 3 * n