English
If you take the first n elements of a sequence and then drop m elements, you get the same result as first dropping m elements and then taking the first n − m elements.
Русский
Если взять первые n элементов последовательноcти, затем удалить m элементов, получится то же самое, что сначала удалить m элементов, а затем взять первые n − m элементов.
LaTeX
$$$$ (\\mathrm{take}\\,n\\,s)\\ \\mathrm{drop}\\,m = (\\mathrm{drop}\\,m\\,s)\\mathrm{take}(n-m). $$$$
Lean4
theorem take_drop {s : Seq α} {n m : ℕ} : (s.take n).drop m = (s.drop m).take (n - m) := by
induction m generalizing n s with
| zero => simp [drop]
| succ k ih =>
cases s
· simp
cases n with
| zero => simp
| succ l =>
simp only [take, destruct_cons, List.drop_succ_cons, Nat.reduceSubDiff]
rw [ih]
congr 1
rw [drop_succ_cons]
