English
The length of the sequence after dropping n elements equals the length of the original sequence minus n (in the extended natural sense).
Русский
Длина последовательности после удаления n элементов равна длине исходной последовательности минус n (в расширенной системе длины).
LaTeX
$$$$ \\mathrm{length}'(\\mathrm{drop}_{n}(s)) = \\mathrm{length}'(s) - n. $$$$
Lean4
@[simp]
theorem drop_length' {n : ℕ} {s : Seq α} : (s.drop n).length' = s.length' - n := by
cases n with
| zero => simp
| succ n =>
cases s with
| nil => simp
| cons x s =>
simp only [drop_succ_cons, length'_cons, Nat.cast_add, Nat.cast_one]
convert drop_length' using 1
generalize s.length' = m
enat_to_nat
omega
