let n, m be Nat; :: thesis: ( n <= m & n <> 0 implies (n + 1) / n >= (m + 1) / m )
assume that
A1: n <= m and
A2: n <> 0 ; :: thesis: (n + 1) / n >= (m + 1) / m
A3: n > 0 by A2;
A4: 1 / n >= 1 / m by A1, A2, XREAL_1:85;
A5: (n + 1) / n = (n / n) + (1 / n)
.= 1 + (1 / n) by A2, XCMPLX_1:60 ;
(m + 1) / m = (m / m) + (1 / m)
.= 1 + (1 / m) by A1, A3, XCMPLX_1:60 ;
hence (n + 1) / n >= (m + 1) / m by A4, A5, XREAL_1:7; :: thesis: verum