proposition: Lemma to_int_pos_surj d : exists n, N.to_hex_int n = norm (Pos d).
proof: Proof. exists (N.of_hex_uint d). unfold N.to_hex_int. now rewrite Unsigned.to_of. Qed.
imports: Hexadecimal HexadecimalFacts HexadecimalPos PArith NArith