feat: BitVec lemmas for smtUDiv, smtSDiv when denominator is zero

[bollu]

This PR is a follow-up to #5609, where we add lemmas characterizing smtUDiv and smtSDiv's behavior when the denominator is zero.

We build some slt theory, connecting it to msb for a clean proof. I chose not to characterize slt in terms of msb a simp lemma, since I anticipate use cases where we want to keep the arithmetic interpretation of slt.

[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 f9048c132d381dfbefe581983d5a93d96c147300 --onto a4fda010f3d44c02393d5afd5cf05509989daf63. (2024-10-04 04:07:12)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase cb40ddad69cada36940844e538ddf09a304b007b --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-08 15:34:19)

[kim-em]

Apologies for the delay. If you can fix the merge conflict we can merge this.

[bollu]

awaiting-review