Fixed and detailed the proof of correctness of quicksort (it may require to increase Z3 timeout)