let n be natural number ; :: thesis: ( n > 1 implies n -' 1 <= (2 * n) -' 3 )
assume A1: n > 1 ; :: thesis: n -' 1 <= (2 * n) -' 3
then A2: n -' 1 = n - 1 by XREAL_1:235;
2 * 1 < 2 * n by A1, XREAL_1:70;
then 2 + 1 <= 2 * n by NAT_1:13;
then A3: (2 * n) -' 3 = (2 * n) - 3 by XREAL_1:235;
n -' 1 > 1 -' 1 by A1, NAT_D:57;
then (n -' 1) + n > 0 + n by XREAL_1:8;
then ((2 * n) - 1) - 1 > n - 1 by A2, XREAL_1:11;
then ((2 * n) - 2) - 1 >= n - 1 by INT_1:79;
hence n -' 1 <= (2 * n) -' 3 by A1, A3, XREAL_1:235; :: thesis: verum