let n be Nat; :: thesis: ( n <> 0 implies (n -' 1) + 1 = (n + 1) -' 1 )
assume n <> 0 ; :: thesis: (n -' 1) + 1 = (n + 1) -' 1
then n >= 1 by NAT_1:14;
then n - 1 >= 1 - 1 by XREAL_1:9;
then (n -' 1) + 1 = (n + (- 1)) + 1 by XREAL_0:def 2
.= (n + 1) - 1 ;
hence (n -' 1) + 1 = (n + 1) -' 1 by XREAL_0:def 2; :: thesis: verum