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

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