for r, s being Real st frac r >= frac s holds
frac (r - s) = (frac r) - (frac s)