mathlib

fc32854b - feat(algebra/order/sub): add `canonically_ordered_add_monoid.to_add_cancel_comm_monoid` (#15955)

feat(algebra/order/sub): add `canonically_ordered_add_monoid.to_add_cancel_comm_monoid` (#15955) We don't have a typeclass for cancellative ordered additive monoids (such as `nat` or finsupps with nat as their codomain). This definition is enough to create the instance mid-proof if needed, so is better than nothing. We already have similar definitions such as `no_zero_divisors.to_cancel_comm_monoid` for rings.