let k be non zero Nat; :: thesis: (k -' 1) + 2 = (k + 2) -' 1
k >= 1 by NAT_2:19;
hence (k -' 1) + 2 = (k + 2) -' 1 by NAT_D:38; :: thesis: verum