proposition: Lemma of_uint_alt d : Pos.of_hex_uint d = of_lu (rev d).
proof: Proof. induction d; simpl; trivial; unfold rev; simpl revapp; rewrite of_lu_revapp; simpl of_lu; try apply of_uint_acc_rev. rewrite IHd. ring. Qed.
imports: Hexadecimal HexadecimalFacts PArith NArith