feat(algebra/ordered_monoid): correct definition (#8877)
Our definition of `ordered_monoid` is not the usual one, and this PR corrects that.
The standard definition just says
```
(mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b)
```
while we currently have an extra axiom
```
(lt_of_add_lt_add_left : ∀ a b c : α, a + b < a + c → b < c)
```
(This was introduced in ancient times, https://github.com/leanprover-community/mathlib/commit/7d8e3f3a6de70da504406727dbe7697b2f7a62ee, with no indication of where the definition came from. I couldn't find it in other sources.)
As @urkud pointed out a while ago [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/ordered_comm_monoid), these really are different.
The second axiom *does* automatically hold for cancellative ordered monoids, however.
This PR simply drops the axiom. In practice this causes no harm, because all the interesting examples are cancellative. There's a little bit of cleanup to do. In `src/algebra/ordered_sub.lean` four lemmas break, so I just added the necessary `[contravariant_class _ _ (+) (<)]` hypothesis. These lemmas aren't currently used in mathlib, but presumably where they are needed this typeclass will be available.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
