feat: getLsb_{rotateLeft, rotateRight}

[bollu]

These will be used by LeanSAT for bitblasting rotations by constant distances.

We first reduce the case when the rotation amount is larger than the width to the case where the rotation amount is less than the width (x.rotateLeft/Right r = x.rotateLeft/Right (r%w)).

Then, we case analyze on the low bits versus the high bits of the rotation, where we prove equality by extensionality.

[leanprover-community-mathlib4-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 73a0c73c7cc465ce8674eacaaa831e9ee0e95950 --onto ff37e5d512efcd3981290270a2fc3ecb100bbd0c. (2024-05-23 12:58:01)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 73a0c73c7cc465ce8674eacaaa831e9ee0e95950 --onto d984030c6a683a80313917b6fd3e77abdf497809. (2024-05-23 14:33:17)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 73a0c73c7cc465ce8674eacaaa831e9ee0e95950 --onto b0c1112471a3f38859d9738184d21132b7d9cd0c. (2024-05-25 01:31:53)

[alexkeizer]

I've golved some of the proofs, but otherwise the proof strategy LGTM

[bollu]

awaiting-review

[semorrison]

Otherwise, I'm happy with the statements and proofs.

[bollu]

@semorrison all comments addressed.