feat: add a lemma relating minKey? and min? for DTreeMap

[wkrozowski]

This PR adds lemmas relating minKey? and min? on the keys list for all DTreeMap and other containers derived from it.

[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 1ae680c5e2f3922ba0c6c257a105426fdab20999 --onto 455fd0b4488e2adc85f825a52e2ee7d944a5740a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-05 21:06:30)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1ae680c5e2f3922ba0c6c257a105426fdab20999 --onto 2ca3bc28590c5c33f755d3bd18252f25ea266266. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-08 11:29:19)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1ae680c5e2f3922ba0c6c257a105426fdab20999 --onto 62f2f9229356039356c0469a46d8ecd77be88e2a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-08 13:15:20)

[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 1ae680c5e2f3922ba0c6c257a105426fdab20999 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-05 21:06:31)

[TwoFX]

I think this would be nice to have as a simp lemma in the reverse direction, called just min?_keys.

[TwoFX]

How hard would it to add also head?_keys saying t.keys.head? = t.minKey?? I hope not too hard given that we know that the list model is sorted and List.min?_eq_head? exists.

[TwoFX]

I guess we also want everything for List.max? and maxKey??