exact h2
case right
a b c : ℤθ
n : ℕ
h : 1 ≤ n
k : ℕ
h2 : ¬3 ^ (k + 1) ∣ 3 * n
s2 : 1 ≤ k
j r : ℕ
hj✝ : 3 * n = 3 ^ k * 3 * r
hj : 3 * n = 3 ^ (k + 1) * r
t1 : j = 3 * r
g : 3 ^ (k + 1) ∣ 3 * n
⊢ ¬3 ^ (k + 1) ∣ 3 * n
no goals