pre(0) = 0
su(pre(x)) = x
pre(su(x)) = x
add(x, 0) = x
add(x, y) = su(add(x, pre(y)))

