proposition: Lemma to_little_uint_succ n d : Nat.to_little_hex_uint n (Little.succ d) = Little.succ (Nat.to_little_hex_uint n d).
proof: Proof. revert d; induction n; simpl; trivial. Qed.
imports: Hexadecimal HexadecimalFacts Arith