mathlib

397d45f2 - feat(algebra/order/monoid): `a + b ≤ c → a ≤ c` (#15033)

feat(algebra/order/monoid): `a + b ≤ c → a ≤ c` (#15033) Generalize four lemmas that were left by previous PRs before `canonically_ordered_monoid` was a thing.