Support ring expressions with exponents

[pi8027]

I have no idea how to do this normalization by reflection though.

[CohenCyril]

Isn't it a matter of reading the Table 1 as reduction rules on the exponents?

[pi8027]

When I put some thought into this, I didn't think so. But now I don't remember the details. Let me do that later. (Now I'm just making my TODOs explicit by putting them as issues.)

[pi8027]

BTW, Lean's ring_exp tactic does not seem to solve (a * b + a * c) ^ n = a ^ n * (b + c) ^ n (not tested). Is there something we can do with such cases?