fact: Fixpoint readBinNAux (s : string) (acc : N) : option N := match s with | "" => Some acc | String c s' => match binDigitToN c with | Some n => readBinNAux s' (2 * acc + n) | None => None end end.
imports: Coq.Strings.String Coq.Strings.Ascii Coq.NArith.NArith