theorem :: PRIMRECI:4

for x, y being Real st 0 <= x & 0 <= y & x <= y ^2 holds
sqrt x <= y