le_sub_one_iff — Mathlib

English

For Fin(n), a - b ≤ a iff b ≤ a.

Русский

Для Fin(n) $a-b\\le a\$ тогда и только тогда, когда $b\\le a\$.

LaTeX

$$$\\forall {n},\\forall {a,b}\\in \\mathrm{Fin}(n),\\ a-b \\le a \\iff b \\le a$$$

Lean4

@[simp]
theorem le_sub_one_iff {k : Fin (n + 1)} : k ≤ k - 1 ↔ k = 0 :=
  by
  cases n
  · simp [fin_one_eq_zero k]
  simp only [le_def]
  rw [← lt_sub_one_iff, le_iff_lt_or_eq, val_fin_lt, val_inj, lt_sub_one_iff, or_iff_left_iff_imp, eq_comm,
    sub_eq_iff_eq_add]
  simp

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