natCast_le_natCast — Mathlib

English

If a ≤ n and b ≤ n, then (a : Fin (n+1)) ≤ b is equivalent to a ≤ b.

Русский

Если a ≤ n и b ≤ n, то (a : Fin (n+1)) ≤ b эквивалентно a ≤ b.

LaTeX

$$$\\forall {a,b,n} \\in \\mathbb{N}, a \\le n \\to b \\le n \\to (a : \\mathrm{Fin}(n+1)) \\le b \\iff a \\le b$$$

Lean4

theorem natCast_le_natCast (han : a ≤ n) (hbn : b ≤ n) : (a : Fin (n + 1)) ≤ b ↔ a ≤ b :=
  by
  rw [← Nat.lt_succ_iff] at han hbn
  simp [le_iff_val_le_val, -val_fin_le, Nat.mod_eq_of_lt, han, hbn]

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