Properties of the successor function