`BookProof.ChapterEulerNState.tailProd_succ` (θ : ℕ → ℝ) (m : ℕ) : tailProd θ (m + 1) = tailProd θ m * Real.sin (θ m) ^ 2

Initializing...

`BookProof.ChapterEulerNState.tailProd_succ` (θ : ℕ → ℝ) (m : ℕ) : tailProd θ (m + 1) = tailProd θ m * Real.sin (θ m) ^ 2 · Prove2Me