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