mathlib

d04db585 - refactor(algebra/order/monoid): Remove redundant field from `ordered_cancel_comm_monoid` (#16445)

refactor(algebra/order/monoid): Remove redundant field from `ordered_cancel_comm_monoid` (#16445) `mul_left_cancel : ∀ a b c, a + b = a + c → b = c` can be inferred from `le_of_mul_le_mul_left : ∀ a b c, a + b ≤ a + c → b ≤ c` and antisymmetry.