theorem :: INT_1:42

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