have : (a' n).val = (a' (n - 1) + a' (n / 2)).val := by
  rw [ZMod.val_add]
  simp_rw [a', a_recurrence n hn]
  rw [ZMod.val]
  simp
n : ℕ
hn : 2 ≤ n
⊢ a' n = a' (n - 1) + a' (n / 2)
n : ℕ
hn : 2 ≤ n
this : (a' n).val = (a' (n - 1) + a' (n / 2)).val
⊢ a' n = a' (n - 1) + a' (n / 2)