fix: nonstandard `Nat` and `Int` instances (#9676)

This PR adds normalizers for nonstandard arithmetic instances. The types
`Nat` and `Int` have built-in support in `grind`, which uses the
standard instances for these types and assumes they are the ones in use.
However, users may define their own alternative instances that are
definitionally equal to the standard ones. This PR normalizes such
instances using simprocs. This situation actually occurs in Mathlib.
Example:

```lean
class Distrib (R : Type _) extends Mul R where

namespace Nat

instance instDistrib : Distrib Nat where
  mul := (· * ·)

theorem odd_iff.extracted_1_4 {n : Nat} (m : Nat)
  (hm : n =
    @HMul.hMul _ _ _ (@instHMul Nat instDistrib.toMul)
      2 m + 1) :
    n % 2 = 1 := by
  grind

end Nat
```