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