lt_add_one_iff — Mathlib

English

For natural n and m in WithBot ENat, n + 1 ≤ m if and only if n < m.

Русский

Для натурального n и m в WithBot ENat: n + 1 ≤ m тогда и только тогда, когда n < m.

LaTeX

$$$$ n + 1 \\le m \\iff n < m $$$$

Lean4

theorem lt_add_one_iff {n : WithBot ℕ∞} {m : ℕ} : n < m + 1 ↔ n ≤ m :=
  by
  rw [← WithBot.coe_one, ← ENat.coe_one, WithBot.coe_natCast, ← Nat.cast_add, ← WithBot.coe_natCast]
  cases n
  · simp only [bot_le, WithBot.bot_lt_coe]
  ·
    rw [WithBot.coe_lt_coe, Nat.cast_add, ENat.coe_one, ENat.lt_add_one_iff (ENat.coe_ne_top _), ← WithBot.coe_le_coe,
      WithBot.coe_natCast]

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