let x, y be Real; :: thesis: ( x >= 0 & y > 0 implies x / ([\(x / y)/] + 1) < y )
assume that
A1: x >= 0 and
A2: y > 0 ; :: thesis: x / ([\(x / y)/] + 1) < y
(x / y) * y < ([\(x / y)/] + 1) * y by A2, INT_1:29, XREAL_1:68;
then A3: x < ([\(x / y)/] + 1) * y by A2, XCMPLX_1:87;
[\(x / y)/] >= 0 by A1, A2, INT_1:53;
hence x / ([\(x / y)/] + 1) < y by A3, XREAL_1:83; :: thesis: verum