feat: port Algebra.Order.Floor (#1304)

This PR provided some of the first serious testing of `linarith` and `abel`, resulting in bugfixes #1358 and #1394.

- [x] depends on: #1392
- [x] depends on: #1394

Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Mathlib.lean

@@ -76,6 +76,7 @@ import Mathlib.Algebra.Order.Field.Canonical.Defs
 import Mathlib.Algebra.Order.Field.Defs
 import Mathlib.Algebra.Order.Field.InjSurj
 import Mathlib.Algebra.Order.Field.Power
+import Mathlib.Algebra.Order.Floor
 import Mathlib.Algebra.Order.Group.Abs
 import Mathlib.Algebra.Order.Group.Bounds
 import Mathlib.Algebra.Order.Group.Defs