theorem LeSqrt: :: PRIMRECI:2

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