feat: introduce drop iterator combinator

[datokrat]

This PR provides the iterator combinator drop that transforms any iterator into one that drops the first n elements.

Additionally, the PR removes the specialized IteratorLoop instance on Take. It currently does not have a LawfulIteratorLoop instance, which needs to exist for the loop consumer lemmas to work. Having the specialized instance is low priority.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 96b81f3cc143d7925c68f4c0f50ff9628befc1e8 --onto 2a1354b3cc1eb05e1b67c656d2172ada8f54a937. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-26 07:53:27)
• 🟡 Mathlib branch lean-pr-testing-8420 build against this PR was cancelled. (2025-05-30 11:03:57) View Log
• ✅ Mathlib branch lean-pr-testing-8420 has successfully built against this PR. (2025-05-30 11:48:40) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0339cd2836fb6f08c4d1e2d2338ed10860a0e081 --onto c6cad5fcff86c6c9ee738bf4faaf643924c587ea. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-02 07:45:59)

[datokrat]

@ Init code owners: If you're wondering why you were notified, the reason is that I'm adding just two small lemmas relating List.drop to List.extract and Array.extract that I couldn't find. You can safely ignore the Std.Data.Iterators files.

[datokrat]

Sorry for automatically notifying you all! During routine rebasing, I forgot to rebase the base branch, so that GitHub detected lots of changes. I have fixed that now, but I can't unsubscribe you again from the PR, unfortunately.