x : ℝ
n : ℕ
⊢ 1 - 2 / 2 ^ 2 - sqrtTwoAddSeries 0 n / 2 ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4

x : ℝ
n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
x : ℝ
n : ℕ
⊢ sin (π / 2 ^ (n + 2)) ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4
rw [sin_sq_pi_over_two_pow, sqrtTwoAddSeries, div_pow, sq_sqrt, add_div, ← sub_sub]
case e_a
x : ℝ
n : ℕ
⊢ 1 - 2 / 2 ^ 2 = 1 / 2

case e_a.e_a
x : ℝ
n : ℕ
⊢ 2 ^ 2 = 4

x : ℝ
n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
x : ℝ
n : ℕ
⊢ 1 - 2 / 2 ^ 2 - sqrtTwoAddSeries 0 n / 2 ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4

x : ℝ
n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
congr
case e_a.e_a
x : ℝ
n : ℕ
⊢ 2 ^ 2 = 4

x : ℝ
n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
case e_a
x : ℝ
n : ℕ
⊢ 1 - 2 / 2 ^ 2 = 1 / 2

case e_a.e_a
x : ℝ
n : ℕ
⊢ 2 ^ 2 = 4

x : ℝ
n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
norm_num
x : ℝ
n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
case e_a.e_a
x : ℝ
n : ℕ
⊢ 2 ^ 2 = 4

x : ℝ
n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
norm_num
case ha
x : ℝ
n : ℕ
⊢ 0 ≤ 2

case hb
x : ℝ
n : ℕ
⊢ 0 ≤ sqrtTwoAddSeries 0 n
x : ℝ
n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n
apply add_nonneg
case hb
x : ℝ
n : ℕ
⊢ 0 ≤ sqrtTwoAddSeries 0 n
case ha
x : ℝ
n : ℕ
⊢ 0 ≤ 2

case hb
x : ℝ
n : ℕ
⊢ 0 ≤ sqrtTwoAddSeries 0 n
norm_num
no goals
case hb
x : ℝ
n : ℕ
⊢ 0 ≤ sqrtTwoAddSeries 0 n
apply sqrtTwoAddSeries_zero_nonneg