English
Let α be a type with a linear order and an addition compatible with the order. Then the extended type WithBot α inherits a right-cancellation property for LT: for any x, y, z in WithBot α, if x + y < x + z, then y < z.
Русский
Пусть α — множество с линейным порядком и операцией сложения, сохраняющей порядок. Тогда расширение WithBot α наследует правое отражение неравенств StrictOrder: для любых x, y, z ∈ WithBot α, если x + y < x + z, то y < z.
LaTeX
$$$$\\forall x,y,z \\in \\mathrm{WithBot}(\\alpha),\\ (x+y) < (x+z) \\Rightarrow y < z.$$$$
Lean4
instance addRightReflectLT [LT α] [AddRightReflectLT α] : AddRightReflectLT (WithBot α) where
elim x y z := by cases x <;> cases y <;> cases z <;> simp [← coe_add, swap]; simpa using lt_of_add_lt_add_right
