for c being Real st c >= 0 holds
c to_power (1 / 2) = sqrt c by Lm39;