[optimization] Reduce common-factor Nat.mod identities before nonlinear SMT solving

A common-factor remainder identity is sent to nonlinear quantified arithmetic instead of reducing during optimization:

```lean
import Blaster
example (z x y : Nat) : (z * x) % (z * y) = z * (x % y) :=
Nat.mul_mod_mul_left z x y

-- Expected to optimize to True; on beta the optimizer leaves a residual goal.
#blaster (only-optimize: 1)
[∀ x y z : Nat, (z * x) % (z * y) = z * (x % y)]
```

This is a performance/optimization gap, not a soundness claim. The existing solver test in `Tests/Smt/SmtNat/SmtNatMod.lean` is sensitive to solver timing: during the beta review it ran for minutes without a process cap and timed out under a 30-second cap in one stack configuration.

Rewrite `(z*x) % (z*y)` to `z*(x%y)`, matching common factors on either side of normalized products. Lean's `Nat.mul_mod_mul_left` validates the rule, including `z = 0` and `y = 0`; no nonzero assumption or division is needed. A numbered regression should check all orientations with optimizer calls and keep the solver test.

Start by reading Tests/Smt/SmtNat/SmtNatMod.lean and running the existing solver test to observe the timing-sensitive case. Then locate the optimizer handling for normalized Nat modulo products and add the requested common-factor identity. Done means numbered optimizer regressions cover all orientations, including zero cases, while the solver test remains.

Written by the indexing model from the issue text.