feat: bv_omega, a simple BitVec->Nat preprocessor + omega

[kim-em]

example (x y z : BitVec 8)
    (hx : x >>> 1 < 16) (hy : y < 16) (hz : z = x + 2 * y) : z ≤ 64 := by
  bv_omega

example (x : BitVec 8) (hx : (x + 1) <<< 1 = 4) : x = 1 ∨ x = 129 := by
  bv_omega

example (x y : BitVec 64) (_ : x < (y.truncate 32).zeroExtend 64) :
    ~~~x > (1#64 <<< 63) := by
  bv_omega

[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 959ad988611db082ae4a97e9b8c4390fab53352e --onto 8b8e001794e6a8b481d37f24fa77bb07797682a1. (2024-02-21 12:40:47)

[nomeata]

Instead of try, this could use { config := { failIfUnchanged := false }}. Is there any reason to prefer the latter over the former? It’s more verbose, but it seems less roundabout than failing first and then recovering. (Maybe it simply doesn’t matter.)