proposition: Lemma of_inj_pos d d' : Nat.of_hex_int (Pos d) = Nat.of_hex_int (Pos d') -> unorm d = unorm d'.
proof: Proof. unfold Nat.of_hex_int. simpl. intros [= H]. apply Unsigned.of_inj. now rewrite <- Unsigned.of_uint_norm, H, Unsigned.of_uint_norm. Qed.
imports: Hexadecimal HexadecimalFacts Arith