let n be Nat; :: thesis: ( 1 <= n implies (n -' 1) + 2 = n + 1 )
assume 1 <= n ; :: thesis: (n -' 1) + 2 = n + 1
hence (n -' 1) + 2 = (n + 2) -' 1 by NAT_D:38
.= ((n + 1) + 1) - 1 by NAT_D:37
.= n + 1 ;
:: thesis: verum