for i, j being Integer st 0 < i & 1 < j holds
i div j < i