Thanks for the great post. Gets me actually excited to learn more Lean. Also the "proof by computation" reminds me so much of this comedy sketch youtu.be/F_OkdTTcO6o?...

Oh interesting. Yeah I think it's very common to define natural numbers without 0, in like "pure" mathematics and in e.g. cs you include 0. I have to check my math book and see how they defined it.
Let me know when you find that theorem would be very interestes

Yeah agreed that there is no right answer. I think the creator of that standard library (looks like Lean, but idk) chose to include 0 because you get some nice properties. Like having an identity element for addition. Do you know if there are any useful properties when you don't include 0?

One of my all-time favorite exchanges on Github is Douglas Crockford telling one of the bootstrap authors "learn to use semicolons properly" and the author responding, "i have learned to use them, [sic] that's why there isn't one present"