mathlib3

fe322e12 - 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.