Theorem mul_le_iff_le_one_right'

feat(algebra/ordered_monoid_lemmas + fixes): consistent use of `covariant` and `contravariant` in `ordered_monoid_lemmas` (#7876) …

feat(algebra/{ordered_monoid, ordered_monoid_lemmas}): split the `ordered_[...]` typeclasses (#7371) …

chore(algebra/ordered_group): move monoid stuff to ordered_monoid.lean (#5066) …

refactor(algebra/ordered_group): multiplicative versions of ordered monoids/groups (#2844) …