have : i = j := Fin.eq_of_val_eq (Nat.le_antisymm ij jl)
case base
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
i j : Fin n
ij : i ≤ j
jl : ↑j ≤ ↑i
h : ¬↑i < ↑i
fi : ↑i ≤ ↑i
⊢ (compare arr[i] arr[j]).isLE = true
case base
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
i j : Fin n
ij : i ≤ j
jl : ↑j ≤ ↑i
h : ¬↑i < ↑i
fi : ↑i ≤ ↑i
this : i = j
⊢ (compare arr[i] arr[j]).isLE = true