feat: offset constraints support for the grind tactic

[leodemoura]

This PR implements support for offset constraints in the grind tactic. Several features are still missing, such as constraint propagation and support for offset equalities, but grind can already solve examples like the following:

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

[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 58cd01154bc6dfae7c0921d04d082efe00856fd1 --onto d2c4471cfa4611977bf4927b5cd849df1a4272b7. (2025-01-11 17:34:52)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 349da6cae2dadcb345d667642958ed8b49ef197c --onto d2c4471cfa4611977bf4927b5cd849df1a4272b7. (2025-01-12 18:38:01)