theorem :: SQUARE_1:37
for a, b being Real st 0 <= b & b < a holds
1 / ((sqrt a) + (sqrt b)) = ((sqrt a) - (sqrt b)) / (a - b)