rw [helper]
case succ.intro
n : ℕ
k : ℤ
hk : a (n + 1) = 2 * k + 1
⊢ a (Nat.succ n + 1) = 2 * (5 * k - 3 * a n + 2) + 1
case succ.intro
n : ℕ
k : ℤ
hk : a (n + 1) = 2 * k + 1
⊢ 5 * a (n + 1) - 6 * a n = 2 * (5 * k - 3 * a n + 2) + 1