chore: fix `bv_omega` regression since v4.9.0 (#4579)

This example, reported from LNSym, started failing when we changed the
definition of `Fin.sub` in
https://github.com/leanprover/lean4/pull/4421.

When we use the new definition, `omega` produces a proof term that the
kernel is very slow on.

To work around this for now, I've removed `BitVec.toNat_sub` from the
`bv_toNat` simp set,
and replaced it with `BitVec.toNat_sub'` which uses the old definition
for subtraction.

This is only a workaround, and I would like to understand why the term
chokes the kernel.

```
example
    (n : Nat)
    (addr2 addr1 : BitVec 64)
    (h0 : n ≤ 18446744073709551616)
    (h1 : addr2 + 18446744073709551615#64 - addr1 ≤ BitVec.ofNat 64 (n - 1))
    (h2 : addr2 - addr1 ≤ addr2 + 18446744073709551615#64 - addr1) :
    n = 18446744073709551616 := by
  bv_omega
```