NB : We do not have
Z.pred (Z.succ n) = n but only
Z.pred (Z.succ n) == n.
It could be possible to consider as canonical only pairs where
one of the elements is 0, and make all operations convert
canonical values into other canonical values. In that case, we
could get rid of setoids and arrive at integers as signed natural
numbers.
NB : Unfortunately, the elements of the pair keep increasing during
many operations, even during subtraction.