by_cases h2: 3 ^ g ∣ 3*n
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
h : 3 ^ g ∣ 3 * n → 3 ^ (g + 1) ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∨ 3 ^ (g + 1) ∣ 3 * n
case pos
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
h : 3 ^ g ∣ 3 * n → 3 ^ (g + 1) ∣ 3 * n
h2 : 3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∨ 3 ^ (g + 1) ∣ 3 * n

case neg
a b c : ℤθ
n : ℕ
j : 1 ≤ n
g : ℕ
h : 3 ^ g ∣ 3 * n → 3 ^ (g + 1) ∣ 3 * n
h2 : ¬3 ^ g ∣ 3 * n
⊢ ¬3 ^ g ∣ 3 * n ∨ 3 ^ (g + 1) ∣ 3 * n