English
Let s be a sequence of elements of α. For every natural number n, the weak sequence obtained by turning s into a weak sequence and dropping the first n elements equals the weak sequence obtained by turning s.drop n into a weak sequence: drop(ofSeq s) n = ofSeq (s.drop n).
Русский
Пусть s — последовательность α. Для каждого натурального n опускание первых n элементов в слабой последовательности, образуемой из s, совпадает с образованием слабой последовательности из s.drop n: drop(ofSeq s) n = ofSeq (s.drop n).
LaTeX
$$$$ \\operatorname{drop}(\\operatorname{ofSeq}(s))\\, n = \\operatorname{ofSeq}(s.\\operatorname{drop}(n)) $$$$
Lean4
@[simp]
theorem dropn_ofSeq (s : Seq α) : ∀ n, drop (ofSeq s) n = ofSeq (s.drop n)
| 0 => rfl
| n + 1 => by
simp only [drop, Seq.drop]
rw [dropn_ofSeq s n, tail_ofSeq]
