English
The tail of a sorted list is sorted with the same relation.
Русский
Хвост отсортированного списка сохраняет ту же сортировку.
LaTeX
$$$\\forall r:\\alpha\\to\\alpha\\to\\text{Prop},\\; \\forall l:\\text{List}(\\alpha),\\; l.\\text{Sorted } r \\Rightarrow l.\\tail\\text{ Sorted } r$$$
Lean4
theorem tail {r : α → α → Prop} {l : List α} (h : Sorted r l) : Sorted r l.tail :=
Pairwise.tail h