theorem :: NAT_2:1

for x, y being Real st x >= 0 & y > 0 holds
x / ([\(x / y)/] + 1) < y