feat: Constructions for splitting and merging vectors of bitvectors

[javra]

This PR provides functions to merge and split vectors of bitvectors, taking up the abandoned #3727.

[javra]

WIP

[javra]

changelog-library

[ghost]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 797b0e2c621d1c9513fefc98429c80f632ea8328 --onto 2edfe2e9cffd55e3c79291628ae091b942291ec9. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-31 12:20:56)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 797b0e2c621d1c9513fefc98429c80f632ea8328 --onto 911ea07a73733650eefa5240652404856bdcceb7. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-02 08:19:02)

[bollu]

LGTM, modulo suggested changes!