for R being Ring
for il being Nat holds SUCC (il,(SCM R)) = {il,(il + 1)}