le_sub_one_of_lt — Mathlib

English

Let a and b be elements of the extended natural numbers with a < b. Then a ≤ b − 1.

Русский

Пусть a и b — элементы расширенного множества натуральных чисел ℕ∞ и выполняется a < b. Тогда a ≤ b − 1.

LaTeX

$$$$\forall a,b \in \mathbb{N}_\infty,\ a < b \implies a \le b - 1.$$$$

Lean4

protected theorem le_sub_one_of_lt (h : a < b) : a ≤ b - 1 :=
  by
  cases b
  · simp
  · exact ENat.le_sub_of_add_le_right one_ne_top <| lt_coe_add_one_iff.mp <| lt_tsub_iff_right.mp h

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