theorem :: SQUARE_1:58

for a, b being Real st a >= 0 holds
sqrt (a + (b ^2)) >= b