proposition: Lemma of_to (z:Z) : Z.of_hex_int (Z.to_hex_int z) = z.
proof: Proof. destruct z; simpl. - trivial. - unfold Z.of_hex_uint. rewrite HexadecimalPos.Unsigned.of_to. now destruct p. - unfold Z.of_hex_uint. rewrite HexadecimalPos.Unsigned.of_to. destruct p; auto. Qed.
imports: Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN ZArith