exact p.get_lt lt
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last k : Fin n
lt : ↑k < first
p : permuted n first (↑last) arr (quickSortImpl arr first last) := quickSortImpl_permuted arr first last
⊢ (quickSortImpl arr first last)[k] = arr[k]
no goals