cases' n
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
hrw : n1 + 1 = 2 * (n - 1) + 1 + 1
⊢ 2 * (n - 1) + 1 + 1 = 2 * n
case zero
hn : a' 0 = 0
hlte : 2 ≤ 0
n1 : ℕ := 2 * (0 - 1) + 1
npos : 0 < 0
hn1v : n1 = 2 * 0 - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hrw : n1 + 1 = 2 * (0 - 1) + 1 + 1
⊢ 2 * (0 - 1) + 1 + 1 = 2 * 0

case succ
n✝ : ℕ
hn : a' (n✝ + 1) = 0
hlte : 2 ≤ n✝ + 1
n1 : ℕ := 2 * (n✝ + 1 - 1) + 1
npos : 0 < n✝ + 1
hn1v : n1 = 2 * (n✝ + 1) - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hrw : n1 + 1 = 2 * (n✝ + 1 - 1) + 1 + 1
⊢ 2 * (n✝ + 1 - 1) + 1 + 1 = 2 * (n✝ + 1)