have ha1 : a' (n1 + 1) = an1 + a' n := by
  have haa : a' (n1 + 1) = a' n1 + a' (n1.succ / 2) := a'_recurrence (n1 + 1) hn2
  have h2n1 : 2 * n / 2 = n := by norm_num
  have h2n1' : (n1 + 1) / 2 = n := by rw [hn1, h2n1]
  rw [haa, h2n1']
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
⊢ ∃ M, n < M ∧ a' M = 0
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
⊢ ∃ M, n < M ∧ a' M = 0