rw [ZMod.val]
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
n : ℕ
hn : 2 ≤ n
⊢ (match (motive := (x : ℕ) → ZMod x → ℕ) 7 with
      | 0 => Int.natAbs
      | n.succ => Fin.val)
      ⟨(a (n - 1) + a (n / 2)) % 7, ⋯⟩ =
    ((match (motive := (x : ℕ) → ZMod x → ℕ) 7 with
          | 0 => Int.natAbs
          | n.succ => Fin.val)
          ⟨a (n - 1) % 7, ⋯⟩ +
        (match (motive := (x : ℕ) → ZMod x → ℕ) 7 with
          | 0 => Int.natAbs
          | n.succ => Fin.val)
          ⟨a (n / 2) % 7, ⋯⟩) %
      7