perf: check each side of `Sym.simp` field identities alone

This PR makes the kernel check of `Sym.simp` arithmetic identities in fields with numeral inverses cheaper. When both sides have the same polynomial with the inverses as atoms, the certificate is the one for commutative rings, without eliminating the inverses. When they have the same rational normal form, each side is normalized alone with the new theorem `eq_true_of_toPolyQ_eq`: eliminating the inverses of each side costs less than eliminating those of both sides from their difference.

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