for a being Real holds a to_power 2 = (- a) to_power 2