le_of_add_le_add_right — Mathlib

English

If z ≠ ⊥ in WithBot α and x + z ≤ y + z, then x ≤ y, assuming LE α and AddRightReflectLE α.

Русский

Если z ≠ ⊥ в WithBot α и x+z ≤ y+z, то x ≤ y, при условии LE α и AddRightReflectLE α.

LaTeX

$$$$\\forall x,y,z \\in \\mathrm{WithBot}(\\alpha),\\ z \\neq \\bot \\;\\Rightarrow\\; (x+z \\le y+z) \\Rightarrow (x \\le y).$$$$

Lean4

protected theorem le_of_add_le_add_right [LE α] [AddRightReflectLE α] (hz : z ≠ ⊥) : x + z ≤ y + z → x ≤ y := by
  lift z to α using hz; cases x <;> cases y <;> simp [← coe_add]; simpa using le_of_add_le_add_right

Похожие утверждения