Library Coq.Numbers.DecimalNat
DecimalNat
Proofs that conversions between decimal numbers and
nat
are bijections.
A few helper functions used during proofs
A direct version of to_little_uint, not tail-recursive
A direct version of of_little_uint
Properties of to_lu
Properties of of_lu
First main bijection result
The other direction
Second bijection result
Some consequences
Conversion from/to signed decimal numbers