feat: min, max, minKey, maxKey, atIndex, getEntryLE, getKeyLE, ... functions for the tree map

[datokrat]

This PR implements the methods min, max, minKey, maxKey, atIndex, getEntryLE, getKeyLE and consorts on the tree map.

In order to implement the proof-based functions such as min and getEntryLT in Queries.lean, it was necessary to extract Balanced and Ordered into new files so that they can be used from Queries.lean.

[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 40c6dfa3ae15457501f8b603128d131a30a3784d --onto ae9d12aeaa075578c7ee3a5a585d0f9fb89cedd2. (2025-02-13 21:57:52)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2649d1510e6f1d1503d8cefbc87470ebdd3b05e1 --onto f50b863868a3625dfbca4fd2ad777d187632b1d4. (2025-02-17 11:06:44)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2649d1510e6f1d1503d8cefbc87470ebdd3b05e1 --onto 88664e4a995883877a5d85211a5cfab0a672b5ed. (2025-02-17 14:03:08)

[TwoFX]

LGTM