for i, j being Integer st i >= 0 & j >= 0 holds
i div j >= 0