let n be Nat; :: thesis: ( n >= 1 implies n -' 1 <= (2 * n) -' 2 )
assume A1: n >= 1 ; :: thesis: n -' 1 <= (2 * n) -' 2
then 2 * 1 <= 2 * n by XREAL_1:64;
then A2: ( 1 * (n -' 1) <= 2 * (n -' 1) & (2 * n) -' 2 = (2 * n) - 2 ) by XREAL_1:64, XREAL_1:233;
n -' 1 = n - 1 by A1, XREAL_1:233;
hence n -' 1 <= (2 * n) -' 2 by A2; :: thesis: verum