have q : ∀ f : ℕ, 3 ^ (f + 1) > 3 * f := by
  intro g
  induction' g with k hk
  norm_num
  change 3 ^ (k + 1 + 1) > 3 * (k + 1)
  have ss : k = 0 ∨ 0 < k := Nat.eq_zero_or_pos k
  cases ss with
  | inl ss =>
  rw [ss]; norm_num
  | inr ss =>
  change 1 ≤ k at ss
  have b : k < 2 * k := by
    change 0 < k at ss
    exact lt_two_mul_self ss
  have q1 : k + 1 < 3 * k :=
    by
    have finall := add_lt_add_of_lt_of_le b ss
    nth_rw 3 [← one_mul k] at finall
    rw [← right_distrib] at finall
    norm_num at finall
    exact finall
  have q2 := lt_trans q1 hk
  rw [pow_succ]
  apply (mul_lt_mul_left zero_lt_three  ).2 q2
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
⊢ 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 : ∀ (f : ℕ), 3 ^ (f + 1) > 3 * f
⊢ False