Please look at the OP. Notice the arithmetic expressions such as "Compute 3 + 4.", which returns "7 : nat" instead of a string of Succ applications to some Zero.
You're arguing against a problem that doesn't exist. Coq is fully capable of understanding decimal arithmetic. The fact that it uses a unary representation in proofs is not a burden that the user has to bear. (It's still a property that they can exploit of course, e.g. in inductive proofs.)
You're arguing against a problem that doesn't exist. Coq is fully capable of understanding decimal arithmetic. The fact that it uses a unary representation in proofs is not a burden that the user has to bear. (It's still a property that they can exploit of course, e.g. in inductive proofs.)