have b : k < 2 * k := by
  change 0 < k at ss
  exact lt_two_mul_self ss
case succ.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
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
⊢ 3 ^ (k + 1 + 1) > 3 * (k + 1)
case succ.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
t : 3 ^ (n + 1) ∣ 3 * n
k : ℕ
hk : 3 ^ (k + 1) > 3 * k
ss : 1 ≤ k
b : k < 2 * k
⊢ 3 ^ (k + 1 + 1) > 3 * (k + 1)