tsub_lt_self — Mathlib

English

If ha is AddLECancellable a and 0 < a and 0 < b, then a − b < a.

Русский

Если a удовлетворяет условию левой отмены и 0 < a, 0 < b, то a − b < a.

LaTeX

$$$\forall a,b\in \alpha\ , AddLECancellable(a) \land 0 < a \land 0 < b \Rightarrow a - b < a$$$

Lean4

protected theorem tsub_lt_self (ha : AddLECancellable a) (h₁ : 0 < a) (h₂ : 0 < b) : a - b < a :=
  by
  refine tsub_le_self.lt_of_ne fun h => ?_
  rw [← h, tsub_pos_iff_lt] at h₁
  exact h₂.not_ge (ha.add_le_iff_nonpos_left.1 <| add_le_of_le_tsub_left_of_le h₁.le h.ge)

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