simp[Nat.or_eq, Nat.le_iff_lt_or_eq, isLeNat]
n : ℕ
i j : Fin n
⊢ ∀ (i_1 : Vector ℕ n),
    ((i_1.get i).isLtNat (i_1.get j)).or ((i_1.get i).isEqNat (i_1.get j)) = (i_1.get i).isLeNat (i_1.get j)
no goals