lt_tsub_iff_right_of_le — Mathlib

English

If c is cancellable and c ≤ b, then a < b − c iff a + c < b.

Русский

Если c канцелируемо и c ≤ b, то a < b − c тогда и только если a + c < b.

LaTeX

$$$ \forall a,b,c \in \alpha,\; AddLECancellable(c) \land c \le b \Rightarrow a < b - c \iff a + c < b $$$

Lean4

protected theorem lt_tsub_iff_right_of_le (hc : AddLECancellable c) (h : c ≤ b) : a < b - c ↔ a + c < b :=
  by
  refine ⟨fun h' => (add_le_of_le_tsub_right_of_le h h'.le).lt_of_ne ?_, hc.lt_tsub_of_add_lt_right⟩
  rintro rfl
  exact h'.ne' hc.add_tsub_cancel_right

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