for i, j, k, l being Nat st k <> 0 & i < l & l <= j & k divides l holds
i div k < j div k