for i being Integer
for r being Real st r <= i holds
[/r\] <= i