chore: add bv_toNat tag for toNat_ofInt

[bollu]

These were missing from the bv_toNat simp-set,
discovered when refactoring LNSym's simp-set:
leanprover/LNSym#208

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5dea30f169b91cdda9a3903a7a9d125e0f075605 --onto a4fda010f3d44c02393d5afd5cf05509989daf63. (2024-10-03 16:21:51)

[bollu]

Aha, I see that BitVec.toNat_sub is intentionally not part of the bv_toNat simp-set:https://github.com/leanprover/lean4/blob/master/src/Init/Data/BitVec/Lemmas.lean#L1935-L1938

-- We prefer this lemma to `toNat_sub` for the `bv_toNat` simp set.
-- For reasons we don't yet understand, unfolding via `toNat_sub` sometimes
-- results in `omega` generating proof terms that are very slow in the kernel.
@[bv_toNat] theorem toNat_sub' {n} (x y : BitVec n) :
    (x - y).toNat = ((x.toNat + (2^n - y.toNat)) % 2^n) := by
  rw [toNat_sub, Nat.add_comm]