for k, n, l being Nat st l >= 1 & n >= k * l holds
n >= k