Merge sort

Summary

Merge sort is a divide-and-conquer sorting algorithm. It splits the list into two halves, sorts each half recursively, and merges the two sorted halves into one sorted list. It uses $O(n \log n)$ comparisons in the worst case, which is optimal for comparison sorts up to a constant factor, and it is stable. Mathlib formalizes it as List.mergeSort.