English
For any sequence s and any n, the first element of the subsequence obtained by dropping the first n elements is precisely the n-th element of the original sequence, when defined.
Русский
Для любой последовательности s и любого n первый элемент подпоследовательности, полученной путём удаления первых n элементов, равен n-й элементу исходной последовательности (если он существует).
LaTeX
$$$$ \\mathrm{head}(\\mathrm{drop}_{n}(s)) = \\mathrm{get?}\,s\,n. $$$$
Lean4
@[simp]
theorem head_dropn (s : Seq α) (n) : head (drop s n) = get? s n := by
induction n generalizing s with
| zero => rfl
| succ n IH => rw [← get?_tail, ← dropn_tail]; apply IH
