feat: push Nat and Int casts through arithmetic in the Sym.Arith normalizer

This PR makes the `Sym.Arith` normalizer push `Nat` and `Int` casts through `+`, `*` and powers with a literal exponent, and for `Int` also through `-`, negation and casts from `Nat`. As a result, `(m + n) • x = m • x + n • x` and `((m * n : Nat) : R) = ((n * m : Nat) : R)` are now proved by `Sym.simp` with `arith`, and by the `grind` normalizer. Truncated `Nat` subtraction, division and remainder are still treated as atoms.

Each push is one step with the existing `Grind.Semiring.natCast_*` and `Grind.Ring.intCast_*` lemmas, applied only when the cast instance and the inner operator's instance are canonical. A cast at the root is normalized too. In a noncommutative structure, the cast's argument is first normalized in `Nat`/`Int`: casts are central, but the normal form there does not reorder them.

Closes #15502

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>