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

[bollu]

This is a follow-up to https://github.com/leanprover/lean4/pull/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.