Insertion sort

Summary

Insertion sort is a simple sorting algorithm that builds the sorted list one element at a time. It inserts each new element into its place among the elements already sorted. It uses $\Theta(n^2)$ comparisons in the worst case but only $n - 1$ on a sorted list. So it is fast on short or nearly sorted lists. It is stable and needs only a constant amount of extra memory. Mathlib formalizes it as List.insertionSort.