Coq is not meant to be a language for computation. If you only use natural numbers to state properties like forall a b: nat, a + b = b + a there is nothing to unfold about them and no need to worry about inefficient computation.
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.