feat: add BitVec.(getMsbD, msb)_(extractLsb', extractLsb), getMsbD_extractLsb'_eq_getLsbD

[luisacicolini]

This PR adds theorems BitVec.(getMsbD, msb)_(extractLsb', extractLsb), getMsbD_extractLsb'_eq_getLsbD.

[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 56733b953eee491cbd1a95018bdb6a76506f5e61 --onto 69a73a18fbfa1fc045bfbf1c4cf93b155d4c9387. (2025-01-27 12:27:39)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 56733b953eee491cbd1a95018bdb6a76506f5e61 --onto 20c616503abe5ce4253c56dbcd7766a91c675ba0. (2025-01-29 13:33:45)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 56733b953eee491cbd1a95018bdb6a76506f5e61 --onto e922edfc218090ab2e54092336c67fe3b970dfc2. (2025-01-30 20:26:30)

[luisacicolini]

changelog-library

[bollu]

Thanks for the API :) I request a couple of minor syntactic changes, and one simplification of a theorem statement.

[bollu]

    (extractLsb hi lo x).msb = (decide (0 < hi - lo + 1) &&
    (decide (lo + (hi - lo) < n) && x.getMsbD (n - 1 - (lo + (hi - lo))))) := by

I feel the conditions can be simplified. We should be able to write decide (0 < hi - lo + 1) as decide (lo <= hi). Similarly, given this, is it not the case that decide (lo + (hi - lo) < n) is equivalent to decide (hi < n), and the final case is x.getMsbD (n - 1 - hi)? Note that I'm not 100% sure about the above computations, but it does seem to me that lo + (hi - lo) is refactorable by using another decide (...) condition if necessary

[alexkeizer]

Some style comments

[luisacicolini]

awaiting-review