add_one_le_iff — Mathlib

English

For n ∈ ℕ and m ∈ WithBot ℕ∞, n + 1 ≤ m if and only if n < m.

Русский

Для n ∈ ℕ и m ∈ WithBot ℕ∞: n + 1 ≤ m эквивалентно n < m.

LaTeX

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

Lean4

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

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