English
Let M be an additive monoid with a preorder and AddLeftStrictMono. Then the positive subset { x in M | 0 < x } inherits right-translation LE: if a ≤ b with a,b > 0, then a + c ≤ b + c for all c > 0 (and similarly on the right).
Русский
Пусть M — аддитивный моноид с упорядочением и AddLeftStrictMono. Тогда множество положительных элементов наследует правое отражение LE: если a ≤ b и a,b > 0, тогда c + a ≤ c + b для всех c > 0 (а также слева).
LaTeX
$$$\\\\forall a,b,c \\\\in \\\\{ x \\\\in M \\\\mid 0 < x \\\\}, a \\\\le b \\\\Rightarrow c + a \\\\le c + b.$$$
Lean4
instance addRightReflectLE [AddRightReflectLE M] : AddRightReflectLE { x : M // 0 < x } :=
⟨fun _ _ _ h => Subtype.coe_le_coe.1 <| le_of_add_le_add_right h⟩
