for r being Real holds [\(frac r)/] = 0