Preferred spelling of cancellative semigroups

Stream: mathlib4

[Eric Wieser]

We currently have docs#LeftCancelSemigroup and docs#RightCancelSemigroup, which extend docs#Semigroup.
We do not have a CancelSemigroup that extends both.

We do however have docs#IsCancelMul, docs#IsLeftCancelMul,and docs#IsRightCancelMul, which are mixins (and so also work for magmas and for semirings)

[Eric Wieser]

/poll Which of the following is preferable?

• Write [CancelSemigroup S], after defining a new CancelSemigroup class and all the boilerplate
• Write [Semigroup S] [IsCancelMul S]
• Write [Semigroup S] [IsCancelMul S] and delete the existing (Left|Right)Cancel versions in favor of [Semigroup S] [IsLeftCancelMul S] etc

[Eric Wieser]

cc @Yaël Dillies, who has already written all the boilerplate for the first option

[Eric Wieser]

I created #8428, which generalizes the existing lemmas about LeftCancelSemigroup to IsLeftCancelMul

[Yaël Dillies]

#8429 contains the result where I have to use a hack to juggle between the two spellings.

[Jireh Loreaux]

I voted for the last option. I don't think it will matter much, but we should benchmark any PR implementing that option.

[Eric Wieser]

It would be great if someone could take a look at #8428 which is a prerequisite for the last option, and for Yael's work

[Eric Wieser]

#8748 is one step closer towards the last poll option