perf: encode `grind` ring certificate numerals as constructor applications

This PR makes the `ToExpr` instances for the polynomials, monomials, and expressions of `Lean.Grind.CommRing` encode numerals as `Int.ofNat n`, `Int.negSucc n`, and raw `Nat` literals, so that the kernel no longer unfolds `OfNat.ofNat` and `Neg.neg` when it evaluates the certificates of the `grind` ring solver and of the `Sym.simp` arithmetic normalizer. Proof terms printed by `grind.debug.proof` now show these constructor applications.

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