feat(algebra/ordered_monoid): min_top_(left|right) (#8880)

Author: pechersky

src/algebra/ordered_monoid.lean

@@ -140,6 +140,10 @@ 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.