for r being Real
for i0 being Integer holds [\r/] + i0 = [\(r + i0)/]