Where does `left_cancel_semigroup` fit into the hierarchy

Stream: maths

[Ben]

Do groups extend left_cancel_semigroup...? Are there any cases of groups where the following does not hold ∀a b c: G, b + a = b + c ↔ a = c...?

[Ruben Van de Velde]

Yeah, group → cancel_monoid → left_cancel_monoid → left_cancel_semigroup

[Ben]

Awesome, do you know how you would define the cancel rule based on groups. I am struggling to follow the implementation in mathlib

[Ben]

I have done it before for natural numbers, but don't know where to start now it is not necessary a inductive datatype

[Junyan Xu]

docs#group doesn't technically extends docs#left_cancel_semigroup or anything with "cancel" in its name, but the instance is provided (proved) at docs#group.to_cancel_monoid.