binary and octal number notations

[JasonGross]

I think it would be nice to support printing and parsing of binary and octal constants in addition to hexadecimal ones. In addition it might make sense to factor out DecimalFacts and HexadecimalFacts to be parameterized over, say,

digits : Type
all_digits : list digits
digit_index : digits -> nat
all_digits_complete : forall d, List.nth_error all_digits (digit_index d) = Some d
all_digits_unique : forall n d, List.nth_error all_digits n = Some d -> digit_index d = n

and then to have proofs about list digits. This should allow compact proofs for all base systems.

cc @proux01, what do you think?

[proux01]

This should indeed be rather straightforward by taking inspiration from coq/coq#11948 your idea seems indeed good and if that works it should avoid most of the bulky duplications that came with hexadecimal numbers.

I don't have neither time nor use for this but if you implement it, I can promise a careful review.