theorem :: PREPOWER:32

for a being Real st a >= 0 holds
2 -Root a = sqrt a