proposition: Lemma of_hex_uint_double d : Pos.of_hex_uint (double d) = N.double (Pos.of_hex_uint d).
proof: Proof. now unfold double; rewrite of_lu_rev, of_lu_double, <-of_lu_rev, rev_rev. Qed.
imports: Hexadecimal HexadecimalFacts PArith NArith