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