proposition: Lemma of_inj_pos d d' : N.of_hex_int (Pos d) = N.of_hex_int (Pos d') -> unorm d = unorm d'.
proof: Proof. unfold N.of_hex_int. simpl. intros [= H]. apply Unsigned.of_inj. change Pos.of_hex_uint with N.of_hex_uint in H. now rewrite <- Unsigned.of_uint_norm, H, Unsigned.of_uint_norm. Qed.
imports: Hexadecimal HexadecimalFacts HexadecimalPos PArith NArith