cases' n
case succ
n : ℕ
hn : 2 ≤ n + 1
⊢ a (n + 1) = a (n + 1 - 1) + a ((n + 1) / 2)
case succ.zero
hn : 2 ≤ 0 + 1
⊢ a (0 + 1) = a (0 + 1 - 1) + a ((0 + 1) / 2)

case succ.succ
n✝ : ℕ
hn : 2 ≤ n✝ + 1 + 1
⊢ a (n✝ + 1 + 1) = a (n✝ + 1 + 1 - 1) + a ((n✝ + 1 + 1) / 2)