let n be Nat; :: thesis: ( n > 1 implies (n -' 2) + 1 = n -' 1 )
assume n > 1 ; :: thesis: (n -' 2) + 1 = n -' 1
then A1: n -' 1 >= 1 by NAT_D:49;
(n -' 2) + 1 = ((n -' 1) -' 1) + 1 by NAT_D:45
.= n -' 1 by A1, XREAL_1:235 ;
hence (n -' 2) + 1 = n -' 1 ; :: thesis: verum