proposition: Lemma to_of (d:int) : Z.to_hex_int (Z.of_hex_int d) = norm d.
proof: Proof. destruct d; simpl; unfold Z.to_hex_int, Z.of_hex_uint. - rewrite <- (HexadecimalN.Unsigned.to_of d). unfold N.of_hex_uint. now destruct (Pos.of_hex_uint d). - destruct (Pos.of_hex_uint d) eqn:Hd; simpl; f_equal. + generalize (HexadecimalPos.Unsigned.to_of d). rewrite Hd. simpl. intros H. symmetry in H. apply unorm_0 in H. now rewrite H. + assert (Hp := HexadecimalPos.Unsigned.to_of d). rewrite Hd in Hp. simpl in *. rewrite Hp. unfold unorm in *. destruct (nzhead d); trivial. generalize (HexadecimalPos.Unsigned.of_to p). now rewrite Hp. Qed.
imports: Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN ZArith