castLT_sub_nezero — Mathlib

English

For i<j in Fin(n), the nonzero property of (j−i).castLT ensures it is nonzero.

Русский

Для i<j в Fin(n) не равенство нулю сохраняется после приведения: (j−i).castLT ≠ 0.

LaTeX

$$$$\text{If } i

Lean4

theorem castLT_sub_nezero {n : ℕ} {i j : Fin n} (hij : i < j) :
    letI : NeZero (n - i.1) := neZero_iff.mpr (by cutsat)
    (j - i).castLT (sub_val_lt_sub (Fin.le_of_lt hij)) ≠ 0 :=
  by
  refine Ne.symm (ne_of_val_ne ?_)
  simpa [coe_sub_iff_le.mpr (Fin.le_of_lt hij)] using by cutsat

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