feat: add `BitVec.(msb, getMsbD)_(rotateLeft, rotateRight)`

[luisacicolini]

This PR adds theorems BitVec.(getMsbD, msb)_(rotateLeft, rotateRight).

We follow the same strategy taken for getLsbD, constructing the necessary auxilliary theorems first (relying on different hypotheses) and then generalizing.

[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 258d3725e73688ef08bc410e4cc8ee91a5641f13 --onto a074bd9a2bd20cc470fbff4f80f2cd7b51ec0d0a. (2024-11-18 17:22:03)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 258d3725e73688ef08bc410e4cc8ee91a5641f13 --onto 5a99cb326c9e9052e135cc63ed02b63371cff6d3. (2024-11-19 09:04:42)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 799b2b662825e646609963921f2c68489b2e664a --onto 4600bb16fcded0356d20ae232e7f8580c56a5955. (2024-11-19 14:10:09)

[kim-em]

@luisacicolini, just a quick request re: the PR description. Thanks for adding a paragraph beginning "This PR ..." --- we know automatically extract these to incorporate in the draft release notes. Having PR authors write them saves us lots of time! But it means that things like "cc: @bollu" need to go in a separate paragraph, otherwise they may end up in the release notes!

[luisacicolini]

got it @kim-em! And thanks for reviewing this :)