for a, b being Real
for c being Nat holds (a / b) to_power c = (a to_power c) / (b to_power c)