`BookProof.ChapterEulerNState.sum_cos_tail` (θ : ℕ → ℝ) (m : ℕ) : ∑ k ∈ Finset.range m, tailProd θ k * Real.cos (θ k) ^ 2 = 1

Initializing...

`BookProof.ChapterEulerNState.sum_cos_tail` (θ : ℕ → ℝ) (m : ℕ) : ∑ k ∈ Finset.range m, tailProd θ k * Real.cos (θ k) ^ 2 = 1 - tailProd θ m · Prove2Me