let n be Nat; :: thesis: ( n > 0 implies ln . ((n + 1) / n) < 1 / n )
assume A1: n > 0 ; :: thesis: ln . ((n + 1) / n) < 1 / n
(n + 1) / n = (n / n) + (1 / n) by XCMPLX_1:62
.= 1 + (1 / n) by A1, XCMPLX_1:60 ;
hence ln . ((n + 1) / n) < 1 / n by Diesel1, A1; :: thesis: verum