feat: Bitvec.{msb, toInt, toFin}_{sdiv, udiv} lemmas

[alexkeizer]

This PR adds toInt and msb lemmas for (un)signed bitvector division.

Todo:

• msb_udiv
• msb_sdiv
• toInt_sdiv

We don't have a toInt_udiv lemma, since the only truly general statement we can make does no better than unfolding the definition, and it's not uncontroversially clear how to unfold toInt (see toInt_eq_msb_cond/toInt_eq_toNat_cond/toInt_eq_toNat_bmod for a few options). Instead, we do have toInt_udiv_of_msb that's able to a more meaningful rewrite given an extra side-condition (that x.msb = false)

Similarly, we do have toFin_udiv, but we don't add toFin_sdiv; the latter can do no better than unfolding the definition, which is an unwieldy match statement.

[alexkeizer]

This PR has been superseded by #6402, the sdiv stuff is still WIP