exact f
case left
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
k : ℕ
hk : 3 * n = 3 ^ g * (3 * k)
f : 3 ^ g ∣ 3 * n
⊢ 3 ^ g ∣ 3 * n

case right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
k : ℕ
hk : 3 * n = 3 ^ g * (3 * k)
f : 3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n
case right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
r1 : ¬3 ^ g ∣ 3 * n
k : ℕ
hk : 3 * n = 3 ^ g * (3 * k)
f : 3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n