cases' hk with j hj
case succ
a b c : ℤθ
k : ℕ
hk : ∃ a, k = 3 * a ∨ k = 3 * a + 1 ∨ k = 3 * a + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2
case succ.intro
a b c : ℤθ
k j : ℕ
hj : k = 3 * j ∨ k = 3 * j + 1 ∨ k = 3 * j + 2
⊢ ∃ a, Nat.succ k = 3 * a ∨ Nat.succ k = 3 * a + 1 ∨ Nat.succ k = 3 * a + 2