CanonicallyOrderedCancelAddCommMonoid

Stream: mathlib4

[Martin Dvořák]

Is there a good reason not to define CanonicallyOrderedCancelAddCommMonoid that would combine OrderedCancelAddCommMonoid and CanonicallyOrderedAddCommMonoid together?
For example NNReal × NNRat × Nat would be a model.

[Martin Dvořák]

Wait. Isn't every CanonicallyOrderedAddCommMonoid cancellative? Lean doesn't show me such a thing but seems reasonable...

[Yaël Dillies]

No, consider Fin n with saturating addition.

[Martin Dvořák]

Ah yes.

[Yaël Dillies]

Honestly, we don't really care about these non-cancellative examples, so you could try adding the axiom to CanonicallyOrderedAddCommMonoid

[Yaël Dillies]

Wait no sorry we do. ℝ≥0∞ and ℕ∞ are not cancellative. But they are basically the only relevant counterexamples.

[Martin Dvořák]

If most examples of CanonicallyOrderedAddCommMonoid are OrderedCancelAddCommMonoid but not all that are relevant for us are, it is a case for defining a CanonicallyOrderedCancelAddCommMonoid. It seems to be a really neat algebra.

[Yaël Dillies]

Yeah sure

[Martin Dvořák]

Have I just gotten ((Yaël Dillies)™)'s preäpproval?

[Martin Dvořák]

Would CanonicallyOrderedCancelCommMonoid (i.e., the multiplicative version) be useful?

[Yaël Dillies]

I think it's fine having if only for symmetry of the API

[Martin Dvořák]

You've heard of the lovely small old round red Italian wooden decorative box?
Now get ready for canonically ordered additive cancellative commutative monoid!
#9307

[Martin Dvořák]

Why is it called CanonicallyOrderedAddCancelCommMonoid specifically? Why is "Add" in the middle of the identifier instead of "AddMonoid" at the end? I chose the name that @[to_additive] allowed.