fix(tactic/ring_exp): `X^(2^3) = X^8` not `X^6` (#18645)
Apparently `ring_exp` didn't correctly handle the exponentiation of coefficients, returning the product instead of the power as a coefficient. It still returned the right `expr`, so the faulty value is only used when checking that two terms are the same and so we can add their coefficients. In other words, this bug could only be triggered when `ring_exp` ends up adding `X^(a^b)` with `X^(a*b)` where `a` and `b` are both numerals.
Thanks to @alainchmt for reporting the bug!
