subtraction in canonically_ordered_add_monoid

Stream: general

[Floris van Doorn]

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]

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]

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

[Floris van Doorn]

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.