have r : ¬3 ^ (n + 1) ∣ 3 * n := by
  clear t; by_contra h
  change ∃ l : ℕ, 3 * n = 3 ^ (n + 1) * l at h
  cases' h with p hp
  rw [hp] at q
  have ss : p = 0 ∨ 0 < p := Nat.eq_zero_or_pos p
  cases ss with
  | inl ss =>
  rw [ss] at hp ; norm_num at hp ; rw [hp] at j ; norm_num at j
  | inr ss =>
  simp at q ; rw [q] at ss ; norm_num at ss
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
⊢ False
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
r : ¬3 ^ (n + 1) ∣ 3 * n
⊢ False