have hn1v : n1 = 2 * n - 1 := lemma1 n npos
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < 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
⊢ ∃ M, n < M ∧ a' M = 0