exact (Nat.not_lt_zero i.val i.isLt).elim
α : 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
no goals