succ_le_of_lt — Mathlib

English

If in a set s the order is inherited, then the successor satisfies y < x implies succ y ≤ x.

Русский

Если в s порядка сохраняется, то для y<x верно succ y ≤ x.

LaTeX

$$$\forall {x,y\in s},\ y

Lean4

theorem succ_le_of_lt {x y : s} (h : y < x) : succ y ≤ x :=
  have hx : ∃ m, (y : ℕ) + m + 1 ∈ s := exists_succ _
  let ⟨k, hk⟩ := Nat.exists_eq_add_of_lt h
  have : Nat.find hx ≤ k := Nat.find_min' _ (hk ▸ x.2)
  show (y : ℕ) + Nat.find hx + 1 ≤ x by cutsat

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