for r, s being Real st 0 <= r & r < s holds
[\(r / s)/] = 0