feat: add BitVec.ult/ule_ofNat

[bollu]

This supersedes leanprover-community/batteries#664, and adds lemmas that mirror ofNat_{add,sub}_ofNat for ult, ule.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b6ed97bb3dad824d3c1fc82dbf290ef0505c42d0 --onto 6719af350fde9339354f28d091458df39a4af9d4. (2024-02-22 02:08:35)

[bollu]

awaiting-review

[joehendrix]

I don't think either of these should be simp rules. There is active work on integrating SAT solving into Lean, and in the ground case, I think it'd be useful to keep the Bitvec types around.

[bollu]

They're no longer simp lemmas.

[bollu]

awaiting-review

[Kha]

@bollu @semorrison Is this still desirable?