# Zulip Chat Archive

## Stream: general

### Topic: subtraction in canonically_ordered_add_monoid

#### Floris van Doorn (Sep 20 2020 at 19:34):

We have a couple instances of `canonically_ordered_add_monoid`

, like `nat`

, `enat`

, `nnreal`

, `ennreal`

, `cardinal`

, `multiset`

, and almost all of them have a `has_sub`

instance, and lemmas about them. In that case `a - b`

is always the minimal `c`

such that `a <= b + c`

.

I think we should just redefine `canonically_ordered_add_monoid`

so that it extends `has_sub`

, and try to prove as much as we can in full generality, to avoid duplication in every individual instance.

There might be things that depend on the linearity of the order, but I see that we recently got `canonically_linear_ordered_add_monoid`

, so we can prove some lemmas for that class. Side note: `canonically_linear_ordered_add_monoid`

is defined but has no instances. We should upgrade some `canonically_ordered_add_monoid`

instances to it.

#### Reid Barton (Sep 21 2020 at 11:33):

I guess it might be worth considering at the same time whether it would be better to have a `has_monus`

or something instead.

Didn't Lean 4 make some change in this area? I forget what it was though.

#### Kevin Buzzard (Sep 21 2020 at 11:53):

Is it called monus because Patrick and I moan about it?

#### Floris van Doorn (Sep 21 2020 at 16:02):

Previous discussions about monus where here:

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/37

https://github.com/leanprover-community/lean/pull/381

No consensus was reached, but there were proponents of the change and (more?) proponents of the status quo.

I think I'll make this change while still using `has_sub`

.

Last updated: May 13 2021 at 23:16 UTC