English
If every element a of l is ≤-related to a (i.e., r a b holds for all b ∈ l), then insertionSort(r, a :: l) = a :: insertionSort(r,l).
Русский
Если для всех b ∈ l следует r a b, то insertionSort(r, a :: l) = a :: insertionSort(r,l).
LaTeX
$$$$ \forall a:\alpha,\forall L:\mathrm{List}(\alpha),\; (\forall b\in L,\; r\ a\ b) \Rightarrow \mathrm{insertionSort}(r,\mathrm{cons}(a,L)) = \mathrm{cons}(a,\mathrm{insertionSort}(r,L)). $$$$
Lean4
theorem insertionSort_cons {a : α} {l : List α} (h : ∀ b ∈ l, r a b) :
insertionSort r (a :: l) = a :: insertionSort r l :=
by
rw [insertionSort]
cases hi : insertionSort r l with
| nil => rfl
| cons b m =>
rw [orderedInsert_of_le]
apply h b <| (mem_insertionSort r).1 _
rw [hi]
exact mem_cons_self
