mathlib3

9b3008eb - feat(algebra/ordered_monoid): inequalities involving mul/add (#6171)

feat(algebra/ordered_monoid): inequalities involving mul/add (#6171) I couldn't find some statements about inequalities, so I'm adding them. I included all the useful variants I could think of.