Eq hardening: additive/multiplicative cancellation reductions

**Goal:** Emit proof steps for the add/mul cancellation reductions in `optimizeEq` (`arithEq?` and the `nat intAddEqReduce? / nat/intMulEqReduce?` family).

**Scope:**
```
x + y = x + z | y + x = x + z | x + y = z + x | y + x = z + x ==> y = z (Nat, Int)
x * y = x * z | y * x = x * z | x * y = z * x | y * x = z * x ==> y = z (Nat, Int; nonZeroInHyps x)
```

**Out of scope:** negation / zero-equals reductions; Bool/Prop rules; the e1 = e2 ==> e2 = e1 reorder.

**DoD:**
- [ ] Each in-scope case pushes its proof step.
- [ ] A variable-operand `#testOptimize [ ..., proof ]` test exercises each case, wired into `Tests/Optimize.lean`.