for n being Nat holds (- tau) to_power ((- 1) * n) = ((- tau) to_power (- 1)) to_power n