fix: make `lia` and `Nat` offset simproc proofs cheap to check in the kernel

This PR changes the proofs produced by `lia`, `grind`, and the `Nat` offset simprocs so that the kernel no longer has to evaluate their arithmetic atoms. Before, for goals containing terms such as `(x + 4294967295) % 4294967296`, the kernel ran in unary `Nat` arithmetic and failed to check the proofs in practice. Closes #16311.

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