let a, b be real positive number ; :: thesis: ( a < b implies sqrt (a / b) < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2))) )
assume A1: a < b ; :: thesis: sqrt (a / b) < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2)))
then a / b < 1 by XREAL_1:191;
then A2: sqrt (a / b) < 1 by SQUARE_1:83, SQUARE_1:95;
sqrt (((a ^2) + (b ^2)) / 2) > 0 by SQUARE_1:93;
then 1 < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2))) by A1, Th3;
hence sqrt (a / b) < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2))) by A2, XXREAL_0:2; :: thesis: verum