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