proposition: Lemma of_int_norm d : Z.of_hex_int (norm d) = Z.of_hex_int d.
proof: Proof. unfold Z.of_hex_int, Z.of_hex_uint. destruct d. - simpl. now rewrite HexadecimalPos.Unsigned.of_uint_norm. - simpl. destruct (nzhead d) eqn:H; [ induction d; simpl; auto; discriminate | destruct (nzhead_nonzero _ _ H) | .. ]; f_equal; f_equal; apply HexadecimalPos.Unsigned.of_iff; unfold unorm; now rewrite H. Qed.
imports: Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN ZArith