English
Let M be an additive monoid with a preorder and AddLeftStrictMono. Then the positive elements { x in M | 0 < x } form a right-cancellative semigroup under addition; that is, for all a,b,c > 0, if a + b = c + b then a = c.
Русский
Пусть M — аддитивный моноид с упорядочением и AddLeftStrictMono. Тогда множество положительных элементов { x ∈ M | 0 < x } с операцией сложения образует правую отменяемую полугруппу; то есть для любых a,b,c > 0, если a + b = c + b, то a = c.
LaTeX
$$$\\\\forall a,b,c \\\\in \\\\{ x \\\\in M \\\\mid 0 < x \\\\}, a + b = c + b \\\\Rightarrow a = c.$$$
Lean4
instance addRightCancelSemigroup {M : Type*} [AddRightCancelMonoid M] [Preorder M] [AddLeftStrictMono M] :
AddRightCancelSemigroup { x : M // 0 < x } :=
fast_instance%Subtype.coe_injective.addRightCancelSemigroup _ coe_add
