let a, b be positive Real; :: thesis: ( a < b implies a / b < sqrt (a / b) )
b ^2 > 0 ;
then b |^ 2 > 0 by NEWTON:81;
then (b |^ 2) * b > 0 ;
then A1: b |^ (2 + 1) > 0 by NEWTON:6;
assume a < b ; :: thesis: a / b < sqrt (a / b)
then a - b < 0 by XREAL_1:49;
then (a * b) * (a - b) < 0 ;
then (((a ^2) * b) - (a * (b ^2))) + (a * (b ^2)) < 0 + (a * (b ^2)) by XREAL_1:8;
then ((a ^2) * b) / (b |^ (2 + 1)) < (a * (b ^2)) / (b |^ (2 + 1)) by A1, XREAL_1:74;
then ((a ^2) * b) / ((b |^ 2) * b) < (a * (b ^2)) / (b |^ (2 + 1)) by NEWTON:6;
then ((a ^2) * b) / ((b |^ 2) * b) < (a * (b ^2)) / ((b |^ 2) * b) by NEWTON:6;
then ((a ^2) * b) / ((b ^2) * b) < (a * (b ^2)) / ((b |^ 2) * b) by NEWTON:81;
then ((a ^2) * b) / ((b ^2) * b) < (a * (b ^2)) / ((b ^2) * b) by NEWTON:81;
then (a ^2) / (b ^2) < (a * (b ^2)) / (b * (b ^2)) by XCMPLX_1:91;
then (a ^2) / (b ^2) < a / b by XCMPLX_1:91;
then (a / b) ^2 < a / b by XCMPLX_1:76;
then sqrt ((a / b) ^2) < sqrt (a / b) by SQUARE_1:27;
hence a / b < sqrt (a / b) by SQUARE_1:22; :: thesis: verum