lean_workbook_plus_29959

Proved

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

$(2)$ $\lfloor x\rfloor -2 \lfloor \frac{x}{2}\rfloor<2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_29959 : ∀ x : ℝ, (Int.floor x - 2 * Int.floor (x / 2)) < 2   :=  by sorry

Source