feat: BitVec.ofNat in grind lia (#11640)

This PR adds support for `BitVec.ofNat` in `grind lia`. Example:

```lean
example (x y : BitVec 8) : y < 254#8 → x > 2#8 + y → x > 1#8 + y := by
  grind
```

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean

@@ -422,6 +422,13 @@ private partial def toInt' (e : Expr) : ToIntM (Expr × Expr) := do
       if let some (k, neZeroInst) ← isFinInstOfNat? inst then
         let h := mkApp2 (mkConst ``Lean.Grind.ofNat_FinZero) k neZeroInst
         return (mkIntLit 0, h)
+    toIntOfNat e n
+  | BitVec.ofNat _ n =>
+    let some n ← getNatValue? n | mkToIntVar e
+    toIntOfNat e n
+  | _ => mkToIntVar e
+where
+  toIntOfNat (e : Expr) (n : Nat) : ToIntM (Expr × Expr) := do
     let some thm ← getOfNatThm? | mkToIntVar e
     let h := mkApp thm (toExpr n)
     if (← hasNumericLoHi) then
@@ -429,8 +436,7 @@ private partial def toInt' (e : Expr) : ToIntM (Expr × Expr) := do
       return (r, h)
     else
       expandWrap e (mkIntLit n) h
-  | _ => mkToIntVar e
-where
+
   toIntBin (toIntOp : ToIntThms) (mkBinOp : Expr → Expr → Expr) (a b : Expr) : ToIntM (Expr × Expr) := do
     unless toIntOp.c?.isSome do return (← mkToIntVar e)
     let (a', h₁) ← toInt' a

tests/lean/run/grind_cutsat_toint_1.lean

@@ -117,3 +117,9 @@ example {n : Nat} (x y : Fin ((n + 1) + 1)) (h₂ : ¬x = y) (h : ¬x < y) : y <
 
 example {n m : Nat} (x : BitVec n) : 2 ≤ n → n ≤ m → m = 2 → x = 0 ∨ x = 1 ∨ x = 2 ∨ x = 3 := by
   grind
+
+example (x : BitVec 8) : x > 2#8 → x > 1#8 := by
+  grind
+
+example (x y : BitVec 8) : y < 254#8 → x > 2#8 + y → x > 1#8 + y := by
+  grind