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

[luisacicolini]

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

[bollu]

@luisacicolini High-level comment: What we do in this proof is to play games to rewrite rotateLeft into rotateLeftAux, while trying to juggle the lsb/msb mismatch. I almost feel that we should write a variant of the getLsb_rotateLeftAux theorems, so we now have a getMsb_rotateLeftAux, and then follow the same proof strategy as we do for getLsb to get the getMsb theorems. I suspect that the proof we have now will adapt (easily?) to prove properties of rotateLeftAux, since we start our proof with:

rw [← rotateLeft_mod_eq_rotateLeft]
...
rw [rotateLeft_eq_rotateLeftAux_of_lt (by assumption)]

So I feel it's worth it to write a clearer proof directly in terms of getMsb_rotateLeftAux

[luisacicolini]

thanok you @bollu. So, if I understand correctly, we now want getMsbD_rotateLeftAux_of_geq, getMsbD_rotateLeftAux_of_le, getMsbD_rotateRightAux_of_geq, getMsbD_rotateRightAux_of_le, right?

[bollu]

@luisacicolini Correct.

[luisacicolini]

Thank you @bollu. I just pushed all the theorems, including the helper ones, following a similar proving strategy as getLsbD theorems.

[bollu]

LGTM, modulo the change I asked for!

[luisacicolini]

I will now close this PR and open one to lean4.