fix: kernel type mismatch in cutsat eq_def proofs

[leodemoura]

This PR fixes a kernel type mismatch raised by lia/grind when internalizing an integer expression whose syntactic structure differs from the structure of its polynomial representation. The mismatch occurred because the eq_def proof term bridged x.denote ctx = e.denote ctx to Poly.denote' ctx p = 0 via a plain Eq.refl e, but Poly.denote' collapses sub-structure such as a trailing + 0 (the (.num 0) monomial is dropped) while e keeps it. The kernel then rejected the application because the equality between x.denote and Poly.denote' p did not hold definitionally.

Closes #13572.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 19baa470e58e04c5832ef7100e9f5de57d9a7704 --onto 0a6c31520b2ebaa6e71227454b46ebfb4986ae7b. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-30 16:15:01)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 19baa470e58e04c5832ef7100e9f5de57d9a7704 --onto 3fc99eef102549c743c6c63547983319bfae6f01. You can force reference manual CI using the force-manual-ci label. (2026-04-30 16:15:04)