constructor
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s3 : ¬3 ^ k ∣ 3 * n
s4 : ¬3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ k ∣ 3 * n ∧ ¬3 ^ k ∣ 3 * n
case left
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s3 : ¬3 ^ k ∣ 3 * n
s4 : ¬3 ^ (k + 1) ∣ 3 * n
⊢ 3 ^ k ∣ 3 * n

case right
a b c : ℤθ
n : ℕ
j : 1 ≤ n
k : ℕ
hk : 3 ^ k ∣ 3 * n
s3 : ¬3 ^ k ∣ 3 * n
s4 : ¬3 ^ (k + 1) ∣ 3 * n
⊢ ¬3 ^ k ∣ 3 * n