let n be Nat; ( n > 1 implies n -' 1 <= (2 * n) -' 3 )
assume A1:
n > 1
; n -' 1 <= (2 * n) -' 3
then
n -' 1 > 1 -' 1
by NAT_D:57;
then A2:
(n -' 1) + n > 0 + n
by XREAL_1:6;
2 * 1 < 2 * n
by A1, XREAL_1:68;
then
2 + 1 <= 2 * n
by NAT_1:13;
then A3:
(2 * n) -' 3 = (2 * n) - 3
by XREAL_1:233;
n -' 1 = n - 1
by A1, XREAL_1:233;
then
((2 * n) - 1) - 1 > n - 1
by A2, XREAL_1:9;
then
((2 * n) - 2) - 1 >= n - 1
by INT_1:52;
hence
n -' 1 <= (2 * n) -' 3
by A1, A3, XREAL_1:233; verum