feat: add BitVec multiplication simp lemmas

[vlad902]

This PR adds BitVec lemmas required to cancel multiplicative negatives, and plumb support through to bv_normalize to make use of this result in the normalized twos-complement form.

I include some bmod lemmas I found useful to prove this result, the two helper lemmas I add use the same naming/proofs as their emod equivalents.

[vlad902]

This is rows 181/182 of the spreadsheet.

[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 1d03cd6a6b9e2cab387692f5ec0d0013b9a9867d --onto ac6a29ee834ba7fd30e9372e51493d7741e9c657. (2025-01-20 22:10:39)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1d03cd6a6b9e2cab387692f5ec0d0013b9a9867d --onto f9e904af5022a57adb6105cda65d1569449346c2. (2025-01-21 19:43:51)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3aea0fd810f404f930aa95f9666cf60940bcf64e --onto 69a73a18fbfa1fc045bfbf1c4cf93b155d4c9387. (2025-01-27 15:04:10)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3aea0fd810f404f930aa95f9666cf60940bcf64e --onto 20c616503abe5ce4253c56dbcd7766a91c675ba0. (2025-01-28 12:49:20)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e7d8948fa6d57e291efb8afd531a6ff6bc2d2318 --onto a35bf7ee4c4d900475d88886825a5337f389bd0f. (2025-01-30 08:28:20)

[hargoniX]

@vlad902 if you fix the merge conflict we can merge this.