>Unary numbers are extremely cumbersome and confusing for proofs, because people are used to working with integers using arithmetic, not pattern matching. "x +

>Unary numbers are extremely cumbersome and confusing for proofs, because people are used to working with integers using arithmetic, not pattern matching. "x + 5" is infinitely better than "Succ(Succ(Succ(Succ(Succ(x)))))“. 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.