cases' s2 with s5 s6
case succ.inr
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s2 : 3 ^ k ∣ 3 * n ∧ 3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ Nat.succ k ∣ 3 * n
case succ.inr.intro
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk s5 : 3 ^ k ∣ 3 * n
s6 : 3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ Nat.succ k ∣ 3 * n