English
For any a and l, insertionSort of (a :: l) equals the take/drop decomposition of insertionSort(r, l) with a inserted in the middle.
Русский
Для любого a и l, сортировка вставками (a :: l) равна разложению по take/drop сортировки вставками применённой к l с вставкой a посередине.
LaTeX
$$$$ \forall (a:\alpha),\forall L:\mathrm{List}(\alpha),\; \mathrm{insertionSort}(r, a :: L) = \big( (\mathrm{insertionSort}(r,L)).\takeWhile(\lambda b. \neg a \preceq b) \big) \\; ++ a :: \big( (\mathrm{insertionSort}(r,L)).\dropWhile(\lambda b. \neg a \preceq b) \big). $$$$
Lean4
theorem insertionSort_cons_eq_take_drop (a : α) (l : List α) :
insertionSort r (a :: l) =
((insertionSort r l).takeWhile fun b => ¬a ≼ b) ++ a :: (insertionSort r l).dropWhile fun b => ¬a ≼ b :=
orderedInsert_eq_take_drop r a _
