[Merged by Bors] - feat: port Order.BoundedOrder

Mathlib.lean

@@ -140,6 +140,7 @@ import Mathlib.Mathport.Attributes
 import Mathlib.Mathport.Rename
 import Mathlib.Mathport.Syntax
 import Mathlib.Order.Basic
+import Mathlib.Order.BoundedOrder
 import Mathlib.Order.Compare
 import Mathlib.Order.GameAdd
 import Mathlib.Order.Iterate