feat: counterexamples for grind linarith module

[leodemoura]

This PR implements counterexamples for grind linarith. Example:

example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c d : α)
    : b ≥ 0 → c > b → d > b → a ≠ b + c → a > b + c → a < b + d →  False := by
  grind

produces the counterexample

a := 7/2
b := 1
c := 2
d := 3

example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b c d : α)
    : a ≤ b → a - c ≥ 0 + d → d ≤ 0 → b = c → a ≠ b → False := by
  grind

generates the counterexample

a := 0
b := 1
c := 1
d := -1

[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 8aa003bdfca4cdb67ab0ac89ff8d85c545cf0525 --onto faffe863343211d03d07d4ef19d90a2aa9d6fc8c. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-13 00:31:28)