Actually, there are binary numbers in the coq standard library. N is in the library NArith and Z is in the library ZArith. Both are binary. Coq is not meant to

Actually, there are binary numbers in the coq standard library. N is in the library NArith and Z is in the library ZArith. Both are binary. 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.