for k, m being Nat
for a being non zero Real holds (a to_power (- k)) * (a to_power (- m)) = a to_power ((- k) - m)