English
Let α be a preorder with additive structure such that addition on the left is strictly monotone and addition on the right is monotone. For all w, x, y, z in WithTop α, if w is not the top element, w ≤ y, and x < z, then w + x < y + z.
Русский
Пусть α — множество с предельным порядком и добавлением, где слева сложение строго монотонно, а справа монотонно. Для любых w, x, y, z в WithTop α, если w ≠ ⊤, и w ≤ y, и x < z, то w + x < y + z.
LaTeX
$$$\\\\forall {\\\\alpha} [Preorder \\\\alpha] [AddLeftStrictMono \\\\alpha] [AddRightMono \\\\alpha] {\\\\,w \\\\,x \\\\,y \\\\,z : WithTop \\\\alpha}, \\\\ (w \\\\neq \top) \\\\to (w \\\\le y) \\\\to (x < z) \\\\to w + x < y + z$$$
Lean4
protected theorem add_lt_add_of_le_of_lt [Preorder α] [AddLeftStrictMono α] [AddRightMono α] (hw : w ≠ ⊤) (hwy : w ≤ y)
(hxz : x < z) : w + x < y + z :=
(WithTop.add_lt_add_left hw hxz).trans_le <| add_le_add_right hwy _
