add_one_le_of_lt

Mathlib.Data.Nat.PartENat

URI: https://scilib.ai/kg/mathlib#PartENat.add_one_le_of_lt

← MathLib Explorer

English

If x < y then x + 1 ≤ y.

Русский

Если x < y, то x+1 ≤ y.

LaTeX

$$$ \forall x,y: \mathrm{PartENat}, x < y \Rightarrow x + 1 \le y$$$

Lean4

theorem add_one_le_of_lt {x y : PartENat} (h : x < y) : x + 1 ≤ y :=
  by
  induction y using PartENat.casesOn
  · apply le_top
  intro h
  rcases ne_top_iff.mp (ne_top_of_lt h) with ⟨m, rfl⟩
  exact_mod_cast Nat.succ_le_of_lt (by norm_cast at h)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru