feat: nonlinear `/` and `%` support in `grind cutsat` (#10010)

This PR improves support for nonlinear `/` and `%` in `grind cutsat`.
For example, given `a / b`, if `cutsat` discovers that `b = 2`, it now
propagates that `a / b = b / 2`. This PR is similar to #9996, but for
`/` and `%`. Example:

```lean
example (a b c d : Nat)
    : b > 1 → d = 1 → b ≤ d + 1 → a % b = 1 → a = 2 * c → False := by
  grind
```