proposition: Lemma of_hex_int_double d : Z.of_hex_int (double d) = Z.double (Z.of_hex_int d).
proof: Proof. now destruct d; simpl; unfold Z.of_hex_uint; rewrite Unsigned.of_hex_uint_double; case Pos.of_hex_uint. Qed.
imports: Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN ZArith