Added automatic proofs +-rightIdentity and x+Sy≡S[x+y].