simp_rw [a', a_recurrence n hn]
n : ℕ
hn : 2 ≤ n
⊢ (a' n).val = ((a' (n - 1)).val + (a' (n / 2)).val) % 7
n : ℕ
hn : 2 ≤ n
⊢ ZMod.val ⟨(a (n - 1) + a (n / 2)) % 7, ⋯⟩ = (ZMod.val ⟨a (n - 1) % 7, ⋯⟩ + ZMod.val ⟨a (n / 2) % 7, ⋯⟩) % 7