exact Nat.ne_of_lt fj
case step_ge.kj.h
α : Type
inst✝ : Ord α
n : Nat
first✝ i✝ j✝ : Fin n
arr : Vec α n
first i j : Fin n
fi✝ : first ≤ i
ij : i ≤ j
fi : first < i
x✝² : ↑first ≤ ↑i - 1
x✝¹ : ¬arr[i] < arr[first]
x✝ : ↑i - 1 ≤ ↑j - 1
ih✝ : (partitionImpl (arr.swap i j) first i.prev j.prev x✝² x✝).snd[first] = (arr.swap i j)[first]
fj : first < j
⊢ ¬↑first = ↑j
no goals