`BookProof.ChapterEulerNState.tailSum_succ` (p : ℕ → ℝ) (n k : ℕ) (h : k < n) : tailSum p n k = p k + tailSum p n (k + 1)

Initializing...

`BookProof.ChapterEulerNState.tailSum_succ` (p : ℕ → ℝ) (n k : ℕ) (h : k < n) : tailSum p n k = p k + tailSum p n (k + 1) · Prove2Me