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