le_of_add_le_add_left — Mathlib

English

If c + a ≤ c + b, then a ≤ b. This is the left-cancellation property of addition with respect to the order.

Русский

Если c + a ≤ c + b, то a ≤ b. Это левое свойство отмены сложения относительно порядка.

LaTeX

$$$$\forall a,b,c \in \mathbb{Z}\sqrt{d},\; c + a \le c + b \Rightarrow a \le b.$$$$

Lean4

protected theorem le_of_add_le_add_left (a b c : ℤ√d) (h : c + a ≤ c + b) : a ≤ b := by
  simpa using Zsqrtd.add_le_add_left _ _ h (-c)

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