[lexpar]

There is an obvious equivalence between unary numbers and binary numbers. Should be quite easy to support inductive proofs with unary numbers while supporting computation with binary numbers, and simply translate between them depending on what context one is in. In fact, I believe this is what Coq does behind the scenes.