Actually I would think that it divides the domain/codomain of the successor function into two disconnected regions. I just "6 is missing" as meaning succ(5) is

Actually I would think that it divides the domain/codomain of the successor function into two disconnected regions. I just "6 is missing" as meaning succ(5) is undefined and that no x exists such that succ(x) = 7. You could probably still prove a lot of conventional math in such a system, except with extra annotations on equations like "given x != 5" much like how we have to add the annotation "given x != 1" on an equation that uses fraction like "y / (x-1)", to avoid invalid derivations from "y / 0". How do you know we're not already in a universe which is missing a number, which is why we have to add annotations constraining denominators to not be zero?