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.)

Natural numbers are used because of the induction principle you get: it's very useful, and generally straightforward to use in lots of contexts (e.g., just the other day I had students proving the correctness of multiplication implemented as iterated addition; the multiplication is over integers, but the inner loop is after you've ensured what you are iterating is non-negative, since you decrement each iteration, and _proving_ it is much more straightforward if you interpret the loop counter as a natural number).

And your point about syntax is also baffling: Coq will display natural numbers as decimal literals, not "S(S(S...".

Have you ever written a proof using decimal numbers? Unary numbers (Peano numbers) only have two cases to match on: Z and Succ. Decimal numbers have at least ten. Even writing proofs for binary numbers in Coq is much more cumbersome than proving things about unary numbers.