feat: Nat equality propagation in grind order

[leodemoura]

This PR implements equality propagation for Nat in grind order. grind order supports offset equalities for rings, but it has an adapter for Nat. Example:

example (a b : Nat) (f : Nat → Int) : a ≤ b + 1 → b + 1 ≤ a → f (1 + a) = f (1 + b + 1) := by
  grind -offset -mbtc -lia -linarith (splits := 0)