Abstract: 
We give a formal proof of the wellknown results about the
number of comparisons performed by two variants of QuickSort: first,
the expected number of comparisons of randomised QuickSort
(i. e. QuickSort with random pivot choice) is
2 (n+1) H_{n} 
4 n, which is asymptotically equivalent to
2 n ln n; second, the number of
comparisons performed by the classic nonrandomised QuickSort has the
same distribution in the average case as the randomised one. 
BibTeX: 
@article{Quick_Sort_CostAFP,
author = {Manuel Eberl},
title = {The number of comparisons in QuickSort},
journal = {Archive of Formal Proofs},
month = mar,
year = 2017,
note = {\url{http://isaafp.org/entries/Quick_Sort_Cost.shtml},
Formal proof development},
ISSN = {2150914x},
}
