natCast_lt_natCast — Mathlib

English

If a ≤ n and b ≤ n, then (a : Fin (n+1)) < b iff 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)) < b \\iff a < b$$$

Lean4

theorem natCast_lt_natCast (han : a ≤ n) (hbn : b ≤ n) : (a : Fin (n + 1)) < b ↔ a < b := by
  rw [← Nat.lt_succ_iff] at han hbn; simp [lt_iff_val_lt_val, Nat.mod_eq_of_lt, han, hbn]

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