fact: Fixpoint to_little_hex_uint p := match p with | 1 => Hexadecimal.D1 Hexadecimal.Nil | p~1 => Hexadecimal.Little.succ_double (to_little_hex_uint p) | p~0 => Hexadecimal.Little.double (to_little_hex_uint p) end.
imports: BinNums