for a, r being Real st r < a & a < [\r/] + 1 holds
frac r < frac a