intro i
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : ¬n > 0
⊢ sortedRange (quickSort' arr) 0 (n - 1)
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
h : ¬n > 0
i : Fin n
⊢ ∀ (j : Fin n), 0 ≤ ↑i → i ≤ j → ↑j ≤ n - 1 → (compare (quickSort' arr)[i] (quickSort' arr)[j]).isLE = true