leRec_succ_left

Mathlib.Data.Nat.Init

URI: https://scilib.ai/kg/mathlib#Nat.leRec_succ_left

Lean4

theorem leRec_succ_left {motive : (m : ℕ) → n ≤ m → Sort*} (refl le_succ_of_le) {m} (h1 : n ≤ m) (h2 : n + 1 ≤ m) :
    -- the `@` is needed for this to elaborate, even though we only provide explicit arguments!
    @leRec _ _ (le_succ_of_le (Nat.le_refl _) refl) (fun _ h ih => le_succ_of_le (le_of_succ_le h) ih) _ h2 =
      leRec (motive := motive) refl le_succ_of_le h1 :=
  by rw [leRec_trans _ _ (le_succ n) h2, leRec_succ']

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

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

Разделы

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

Аффилиация

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