#398 Rewrite rule for recursive exponentiation

[Guillaume Verdier]

Currently, the only rewrite rules on exponents define base cases: E^1=E, 1^E=1, E^0=1.
If we have E^n, we can't do anything with it in proofs. We should at least have a rewrite rule E^n=E*E^(n-1), for n>0.

[Guillaume Verdier]

This rule has been implemented and merged in commit [53cd8c].