use 5*k - 3*a n + 2
case succ.intro
n : ℕ
k : ℤ
hk : a (n + 1) = 2 * k + 1
⊢ odd (a (Nat.succ n + 1))
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