`BookProof.ChapterEulerCountableChain.one_sub_condCos` (θ : ℕ → ℝ) (n : ℕ) : 1 - condCos θ n = Real.sin (θ n) ^ 2

Initializing...

`BookProof.ChapterEulerCountableChain.one_sub_condCos` (θ : ℕ → ℝ) (n : ℕ) : 1 - condCos θ n = Real.sin (θ n) ^ 2 · Prove2Me