Emit proof steps for Int constant folding

**Goal:** Int constant folding emits no proof step, so goals such as `2 - 2 + b = b` fall back to `blasterProven`.

**Scope:**
```
N1 + N2 ==> N1 "+" N2, N1 * N2 ==> N1 "*" N2, - N ==> "-" N
(optimizeIntAdd / Mul / Neg)
Int.sub unfolding to m + -n (normConst, OptimizeConst.lean)
Same fold inside the associativity branches (cstAddProp? / cstMulProp?)
```

**DoD:**
- [ ] Each fold above pushes its proof step.
- [ ] A `#testOptimize [ ..., proof ]` test exercises each case, wired into `Tests/Optimize.lean`.
- [ ] No regression in the `OptimizeInt` suites.