left
case h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ Nat.succ k = 3 * (j + 1) ∨ Nat.succ k = 3 * (j + 1) + 1 ∨ Nat.succ k = 3 * (j + 1) + 2
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
⊢ Nat.succ k = 3 * (j + 1)