let a, b be real positive number ; :: thesis: ( a < b implies a / b < sqrt (a / b) )
b ^2 > 0 ;
then b |^ 2 > 0 by NEWTON:100;
then (b |^ 2) * b > 0 ;
then A1: b |^ (2 + 1) > 0 by NEWTON:11;
assume a < b ; :: thesis: a / b < sqrt (a / b)
then a - b < 0 by XREAL_1:51;
then (a * b) * (a - b) < 0 ;
then (((a ^2) * b) - (a * (b ^2))) + (a * (b ^2)) < 0 + (a * (b ^2)) by XREAL_1:10;
then ((a ^2) * b) / (b |^ (2 + 1)) < (a * (b ^2)) / (b |^ (2 + 1)) by A1, XREAL_1:76;
then ((a ^2) * b) / ((b |^ 2) * b) < (a * (b ^2)) / (b |^ (2 + 1)) by NEWTON:11;
then ((a ^2) * b) / ((b |^ 2) * b) < (a * (b ^2)) / ((b |^ 2) * b) by NEWTON:11;
then ((a ^2) * b) / ((b ^2) * b) < (a * (b ^2)) / ((b |^ 2) * b) by NEWTON:100;
then ((a ^2) * b) / ((b ^2) * b) < (a * (b ^2)) / ((b ^2) * b) by NEWTON:100;
then (a ^2) / (b ^2) < (a * (b ^2)) / (b * (b ^2)) by XCMPLX_1:92;
then (a ^2) / (b ^2) < a / b by XCMPLX_1:92;
then (a / b) ^2 < a / b by XCMPLX_1:77;
then sqrt ((a / b) ^2) < sqrt (a / b) by SQUARE_1:95;
hence a / b < sqrt (a / b) by SQUARE_1:89; :: thesis: verum