### Quicksort: inductive proof of correctness

```
;;; things is a list of length n+1
;;; list? is a total order on those things
(define (quicksort things less?)
(if (< (length things) 2)
things
(let ((pivot (first things))
(other (rest things)))
(let-values (((below above)
(partition (lambda (x)
(less? x pivot))
other)))
(append (quicksort below less?)
(list pivot)
(quicksort above less?))))))
```

If we sort the elements that are `below`

the `pivot`

, and also sort the elements
in the list `above`

, and place the
`pivot`

in between those sorted sublists,
we'll get the correct result.

That correct result is computed and returned by the highlighted call
to `append`

, which completes our proof of IH(n+1).

That in turn completes of our proof of
*if IH(n) then IH(n+1)*.
We didn't assume anything at all about
the natural number n, so we have proved
*(∀ n) if IH(n) then IH(n+1)*.

That was the second of the two antecedents we needed to
prove before we could apply the rule of inference for
induction. Having proved both antecedents of that rule,
we get to infer the consequent:
*(∀ n) IH(n)*.

That says `quicksort`

returns the correct result
no matter how long a list you give it.