feat: literals, lower and upper bounds in the offset constraint module within grind

[leodemoura]

This PR adds support for numerals, lower & upper bounds to the offset constraint module in the grind tactic. grind can now solve examples such as:

example (f : Nat → Nat) :
        f 2 = a →
        b ≤ 1 → b ≥ 1 →
        c = b + 1 →
        f c = a := by
  grind

In the example above, the literal 2 and the lower&upper bounds, b ≤ 1 and b ≥ 1, are now processed by offset constraint module.

[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 5d6bf75795c7efa1e6346b77e1762d1f9d0adc63 --onto e9bd9807ef7a983365df9ac55d35040d0b2d5ef2. (2025-01-15 02:57:19)