fact: Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N) {struct p} : to_N (of_pos p rest) base = to_N rest match base with | N0 => N.pos p | Npos v => Npos (pos_bin_app v p) end.
imports: Ascii String BinNums