Prove2Me

Combining two rational terms involving a natural power

Proved
WorkbookSource.problem_19563

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Prove that: S1=nn+1−n(n+1)nn=n(nn−1)nn(n+1)S_1=\frac{n}{n+1}-\frac{n}{(n+1)n^n}=\frac{n(n^n-1)}{n^n(n+1)}

Source: InternLM Lean-Workbook, record lean_workbook_19563 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_19563 (n : ℕ) (hn : n ≠ 0) : (n : ℝ) / (n + 1) - (n : ℝ) / ((n + 1) * n ^ n) = (n * (n ^ n - 1)) / (n ^ n * (n + 1))  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_19563; Apache-2.0

View graph