English
If a finite sequence l has the property that each consecutive pair is related by R, then removing the first n elements preserves the chain property.
Русский
Если конечная последовательность l образует цепь по отношению R (то есть пары соседних элементов удовлетворяют R), то удаление первых n элементов сохраняет свойство цепи.
LaTeX
$$$\\forall \\{\\alpha\\}, \\forall R:\\, \\alpha \\to \\alpha \\to \\mathrm{Prop}, \\forall l:\\, \\text{List }\\alpha,\\ IsChain\\, R\\, l \\rightarrow \\forall n:\\, \\mathbb{N}, \\ IsChain\\, R\\, (\\text{drop } n\\, l) $$$
Lean4
theorem drop (h : IsChain R l) (n : ℕ) : IsChain R (drop n l) :=
h.suffix (drop_suffix _ _)
