English
If l is sorted with respect to r, then insertionSort(r,l) = l; i.e., sorting does nothing to an already sorted list.
Русский
Если список l упорядочен относительно r, то сортировка вставками не меняет его.
LaTeX
$$$$ \forall l:\mathrm{List}(\alpha),\; \mathrm{Sorted}(r,l) \Rightarrow \mathrm{insertionSort}(r,l) = l. $$$$
Lean4
/-- If `l` is already `List.Sorted` with respect to `r`, then `insertionSort` does not change
it. -/
theorem insertionSort_eq : ∀ {l : List α}, Sorted r l → insertionSort r l = l
| [], _ => rfl
| [_], _ => rfl
| a :: b :: l, h => by
rw [insertionSort, Sorted.insertionSort_eq, orderedInsert, if_pos]
exacts [rel_of_sorted_cons h _ mem_cons_self, h.tail]
