for r, s being Real st frac r < frac s holds
frac (r - s) = ((frac r) - (frac s)) + 1