for k, n being Nat st k > 0 & n div k = 0 holds
n < k