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