feat: add a FloorSemiring instance to NNRat

[eric-wieser]

Also some missing norm_cast lemmas for inequalities of casts between different types.

---

• depends on: [Merged by Bors] - feat: order lemmas for NNRat #13547

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: order lemmas for NNRat #13547
  By Dependent Issues (🤖). Happy coding!

[github-actions]

PR summary 6d6f59bbac

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Data.NNRat.Floor	586

---

Declarations diff

+ cast_le_intCast
+ cast_lt_intCast
+ ceil_cast
+ ceil_coe
+ coe_ceil
+ coe_floor
+ den_one
+ den_zero
+ floor_cast
+ floor_coe
+ floor_def
+ floor_intCast_div_natCast
+ instance : FloorSemiring ℚ≥0
+ intCast_le_cast
+ intCast_lt_cast
+ intCeil_cast
+ intFloor_cast
+ natFloor_natCast_div_natCast
+ num_one
+ num_zero
++ cast_le_natCast
++ cast_lt_natCast
++ floor_natCast_div_natCast
++ natCast_le_cast
++ natCast_lt_cast

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

[YaelDillies]

Doesn't that mean we are missing Nat.fract with the obvious definition?

[eric-wieser]

Yeah, but adding new definitions seems out of scope for a PR that adds new instances.

[YaelDillies]

Can you add the same lemmas comparing Nat.cast and Int.cast? (I think they are also missing?)

[eric-wieser]

I want to declare this out of scope for a PR about NNRat.

[YaelDillies]

Thanks!

maintainer merge

[github-actions]

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

[urkud]

Otherwise LGTM. Thanks!
bors d+

[mathlib-bors]

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

[jcommelin]

bors r+

[mathlib-bors]

Build failed (retrying...):

• Build

[sgouezel]

bors r-

[mathlib-bors]

Canceled.

[sgouezel]

Can you merge master, fix the build, and send it back to bors?
bors d+

[mathlib-bors]

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