drop_succ_cons — Mathlib

English

Dropping n + 1 elements from a sequence constructed by prepending an element x to a sequence s is the same as dropping n elements from s.

Русский

Удаление n + 1 элементов из последовательности, построенной добавлением головы x к s, эквивалентно удалению n элементов из s.

LaTeX

$$$$ \\mathrm{drop}_{n+1}(\\mathrm{cons}(x,s)) = \\mathrm{drop}_{n}(s). $$$$

Lean4

@[simp]
theorem drop_succ_cons {x : α} {s : Seq α} {n : ℕ} : (cons x s).drop (n + 1) = s.drop n := by simp [← dropn_tail]

Похожие утверждения