lean_workbook_plus_35030

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Investigate the inequality $x[\frac{k-1}{x}]-(x+1)[\frac{k}{x+1}]\leq 0$ for all positive integers $k$ and positive real numbers $x$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_35030 (x : ℝ) (k : ℤ) (hx : 0 < x) (hk : 0 < k) : x * (k - 1) / x - (x + 1) * k / (x + 1) ≤ 0   :=  by sorry

Source