for n being Nat st n > 0 holds
ln . ((n + 1) / n) < 1 / n