feat: add difference on DTreeMap/TreeMap/TreeSet [Work in progress]

[wkrozowski]

This PR adds support for difference operation for DHashMap/HashMap/HashSet and proves several lemmas about it.

Stacked on top of #11212, and requires #11165 to be merged first

[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 bef8574b93cacb87c7e9804870341441346a64b5 --onto 8b575dcbf2a3b907044df2233a61b61003eeeb45. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-17 17:59:57)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4296f8deeece4fdf6dbe7d5d6b5e23bd6a250d13 --onto 5a4226f2bdcc6299df76285b1d30f238546c09fe. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-18 16:39:38)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase bef8574b93cacb87c7e9804870341441346a64b5 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-17 17:59:58)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 4296f8deeece4fdf6dbe7d5d6b5e23bd6a250d13 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-18 16:39:40)