Comment by inigyou

I think this works, but I could be proven wrong yet again.

You might also want to prove that the comparison implements a strict total order, but that would be part of the comparison's spec, not the sorting function's. There is another possibility for a mistake there: if you don't use exactly the same test, you might prove that your < implements a strict total order by its definition, while also proving it doesn't according to the sort function spec and thus allowing the sort to return anything.