rw [← add_assoc]
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
babymath : 3 = 2 + 1
⊢ k + 1 = 3 * j + (2 + 1)
case h.h
a b c : ℤθ
k j : ℕ
h3 : k = 3 * j + 2
babymath : 3 = 2 + 1
⊢ k + 1 = 3 * j + 2 + 1