lt_of_tsub_lt_tsub_right_of_le — Mathlib

English

For a, b, c with c ≤ b, if a − c < b − c, then a < b.

Русский

Для a, b, c с c ≤ b, если a − c < b − c, то a < b.

LaTeX

$$$ c \\le b \\Rightarrow a - c < b - c \\Rightarrow a < b $$$

Lean4

/-- See `lt_of_tsub_lt_tsub_right` for a stronger statement in a linear order. -/
theorem lt_of_tsub_lt_tsub_right_of_le (h : c ≤ b) (h2 : a - c < b - c) : a < b :=
  by
  refine ((tsub_le_tsub_iff_right h).mp h2.le).lt_of_ne ?_
  rintro rfl
  exact h2.false

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