Commit 2024-07-21 16:25 c5da640e

feat(Order/Floor): x - 1 / 2 < round x (#14964) Adding a new theorem to Mathlib/Algebra/Order/Floor.lean :

theorem round_half_bot : a - (1 / 2 : ℚ) < round a := by
  rw [round_eq, show (a - 1 / 2 : ℚ) = (a + 1 / 2) - 1 by ring]
  exact Int.sub_one_lt_floor (a + 1 / 2)