chore(order): generalize min_top_left (#10486)

As well as its relative `min_top_right`.
Also provide `max_bot_(left|right)`.

src/algebra/order/monoid.lean

@@ -117,10 +117,6 @@ lemma top_add (a : α) : ⊤ + a = ⊤ := linear_ordered_add_comm_monoid_with_to
 lemma add_top (a : α) : a + ⊤ = ⊤ :=
 trans (add_comm _ _) (top_add _)
 
--- TODO: Generalize to a not-yet-existing typeclass extending `linear_order` and `order_top`
-@[simp] lemma min_top_left (a : α) : min (⊤ : α) a = a := min_eq_right le_top
-@[simp] lemma min_top_right (a : α) : min a ⊤ = a := min_eq_left le_top
-
 end linear_ordered_add_comm_monoid_with_top
 
 /-- Pullback an `ordered_comm_monoid` under an injective map.

src/order/bounded_order.lean

@@ -1015,6 +1015,17 @@ end
 
 end bounded_order
 
+section linear_order
+
+variables [linear_order α]
+
+lemma min_top_left [order_top α] (a : α) : min (⊤ : α) a = a := min_eq_right le_top
+lemma min_top_right [order_top α] (a : α) : min a ⊤ = a := min_eq_left le_top
+lemma max_bot_left [order_bot α] (a : α) : max (⊥ : α) a = a := max_eq_right bot_le
+lemma max_bot_right [order_bot α] (a : α) : max a ⊥ = a := max_eq_left bot_le
+
+end linear_order
+
 section distrib_lattice_bot
 variables [distrib_lattice α] [order_bot α] {a b c : α}