feat: remove runtime bounds checks and partial from qsort

[kim-em]

This PR refactors Array.qsort to remove runtime array bounds checks, and avoids the use of partial. We use the Vector API, along with auto_params, to avoid having to write any proofs. The new code benchmarks indistinguishably from the old.

[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 88e3a2b1ab287020d5a393dc53c9441aa868681f --onto 9a17919ef11c2dba824498229633b8333a0b53d9. (2024-11-28 01:01:12)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 88e3a2b1ab287020d5a393dc53c9441aa868681f --onto 27df5e968a675780a7bcd105a19774c0c59295d8. (2024-12-01 06:28:13)