constructor
case h
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 + 2)
t3 : j = 3 * r + 2
⊢ 1 ≤ k ∧ (3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2))
case h.left
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 + 2)
t3 : j = 3 * r + 2
⊢ 1 ≤ k

case h.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 + 2)
t3 : j = 3 * r + 2
⊢ 3 * ↑n = 3 ^ k * (3 * ↑r + 1) ∨ 3 * ↑n = 3 ^ k * (3 * ↑r + 2)