proposition: Lemma double_to_hex_int n : double (Z.to_hex_int n) = Z.to_hex_int (Z.double n).
proof: Proof. now rewrite <-(of_to n), <-of_hex_int_double, !to_of, double_norm. Qed.
imports: Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN ZArith