refactor(algebra/order/monoid): use typeclasses instead of lemmas (#14848)
refactor(algebra/order/monoid): use typeclasses instead of lemmas (#14848)

Use `covariant_class`/`contravariant_class` instead of type-specific `mul_le_mul_left` etc lemmas. Also, rewrite some proofs to use API about inequalities on `with_top`/`with_bot` instead of the exact form of the current definition.





leanprover-community/mathlib,leanprover-community/mathlib