English
Let a,b,c be elements of WithBot(WithTop α) with α additive and ordered; if c ≠ ⊥ and c ≠ ⊤, then a + c ≤ b + c iff a ≤ b.
Русский
Пусть a,b,c ∈ WithBot(WithTop α) с аддитивной структурой и порядком; если c не ⊥ и не ⊤, тогда a+c ≤ b+c экв. a ≤ b.
LaTeX
$$$$\\forall a,b,c \\in \\mathrm{WithBot}(\\mathrm{WithTop}(\\alpha)),\\ c \\neq \\bot,\\ c \\neq \\top \\Rightarrow (a+c \\le b+c) \\iff (a \\le b).$$$$
Lean4
/-- Addition in `WithBot (WithTop α)` is right cancellative provided the element
being cancelled is not `⊤` or `⊥`.
-/
theorem add_le_add_iff_right' {α : Type*} [Add α] [LE α] [AddRightMono α] [AddRightReflectLE α]
{a b c : WithBot (WithTop α)} (hc : c ≠ ⊥) (hc' : c ≠ ⊤) : a + c ≤ b + c ↔ a ≤ b := by
induction a <;> induction b <;> induction c <;> norm_cast at * <;>
aesop (add simp WithTop.add_le_add_iff_right)
-- There is no `WithBot.map_mul_of_mulHom`, since `WithBot` does not have a multiplication.
