[Merged by Bors] - feat(Order/Floor): x - 1 / 2 < round x

[Colin166]

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)

[github-actions]

PR summary 5b76afbd63

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ round_le_add_half
+ sub_half_lt_round

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[Command-Master]

Additionally both theorems should be moved to the LinearOrderedField section, after round_eq

[kim-em]

This pulls in additional imports to a file making basic definitions. Please move to a later or new file.

[Colin166]

Without import Mathlib.Tactic.Ring Lean doesn't recognize ring as a valid tactic; that's why I included it. I will try to prove the goal in a different way.

[Colin166]

Alright issue should be fixed. I replaced ring with nlinarith

[YaelDillies]

Thanks!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[urkud]

Please update the commit message to reflect name changes. Otherwise LGTM. Thanks!
bors d+

P.S.: Also, no need to include proofs in the commit message. It's enough to list lemma names.

[mathlib-bors]

✌️ Colin166 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[Colin166]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style