`BookProof.ChapterE2.remainder_succ` (θ : ℕ → ℝ) (N : ℕ) : remainder θ (N + 1) = remainder θ N * Real.sin (θ N) ^ 2

Initializing...

`BookProof.ChapterE2.remainder_succ` (θ : ℕ → ℝ) (N : ℕ) : remainder θ (N + 1) = remainder θ N * Real.sin (θ N) ^ 2 · Prove2Me