if h : n > 0 then
  simp [quickSort', h]
  apply quickSortImpl_sortedRange
else
  intro i
  have : n = 0 := Nat.eq_zero_of_not_pos h
  subst n
  exact (Nat.not_lt_zero i.val i.isLt).elim
α : Type
inst✝ : Order α
n : Nat
arr : Vec α n
⊢ sortedRange (quickSort' arr) 0 (n - 1)
no goals