Post #2404681

@boarders@mathstodon.xyz hell, I'll even grant that either choice is more natural in different contexts: 0 isn't natural when you're constructing the primes to play with, but if you're a Peano fan in a higher-order setting it can't help but be the default