fact: Definition ascii_to_digit (ch : ascii) : option N := (if ascii_dec ch "0" then Some 0 else if ascii_dec ch "1" then Some 1 else if ascii_dec ch "2" then Some 2 else if ascii_dec ch "3" then Some 3 else if ascii_dec ch "4" then Some 4 else if ascii_dec ch "5" then Some 5 else if ascii_dec ch "6" then Some 6 else if ascii_dec ch "7" then Some 7 else None)%N.
imports: Ascii String BinNums