Hexadecimal: proofs that conversions from/to nat,N,Z and Q are bijections

7 files changed, 1895 insertions, 0 deletions

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 8db6b63273..7896b59a8b 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -239,6 +239,12 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/DecimalZ.v
     theories/Numbers/DecimalQ.v
     theories/Numbers/DecimalString.v
+    theories/Numbers/HexadecimalFacts.v
+    theories/Numbers/HexadecimalNat.v
+    theories/Numbers/HexadecimalPos.v
+    theories/Numbers/HexadecimalN.v
+    theories/Numbers/HexadecimalZ.v
+    theories/Numbers/HexadecimalQ.v
     </dd>
 
     <dt> <b>&nbsp;&nbsp;NatInt</b>:
diff --git a/theories/Numbers/HexadecimalFacts.v b/theories/Numbers/HexadecimalFacts.v
new file mode 100644
index 0000000000..7328b2303d
--- /dev/null
+++ b/theories/Numbers/HexadecimalFacts.v
@@ -0,0 +1,340 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** * HexadecimalFacts : some facts about Hexadecimal numbers *)
+
+Require Import Hexadecimal Arith.
+
+Scheme Equality for uint.
+
+Scheme Equality for int.
+
+Lemma rev_revapp d d' :
+  rev (revapp d d') = revapp d' d.
+Proof.
+  revert d'. induction d; simpl; intros; now rewrite ?IHd.
+Qed.
+
+Lemma rev_rev d : rev (rev d) = d.
+Proof.
+  apply rev_revapp.
+Qed.
+
+Lemma revapp_rev_nil d : revapp (rev d) Nil = d.
+Proof. now fold (rev (rev d)); rewrite rev_rev. Qed.
+
+Lemma app_nil_r d : app d Nil = d.
+Proof. now unfold app; rewrite revapp_rev_nil. Qed.
+
+Lemma app_int_nil_r d : app_int d Nil = d.
+Proof. now case d; intro d'; simpl; rewrite app_nil_r. Qed.
+
+Lemma revapp_revapp_1 d d' d'' :
+  nb_digits d <= 1 ->
+  revapp (revapp d d') d'' = revapp d' (revapp d d'').
+Proof.
+  now case d; clear d; intro d;
+    [|case d; clear d; intro d;
+      [|simpl; case nb_digits; [|intros n]; intros Hn; exfalso;
+        [apply (Nat.nle_succ_diag_l _ Hn)|
+         apply (Nat.nle_succ_0 _ (le_S_n _ _ Hn))]..]..].
+Qed.
+
+Lemma nb_digits_pos d : d <> Nil -> 0 < nb_digits d.
+Proof. now case d; [|intros d' _; apply Nat.lt_0_succ..]. Qed.
+
+Lemma nb_digits_revapp d d' :
+  nb_digits (revapp d d') = nb_digits d + nb_digits d'.
+Proof.
+  now revert d'; induction d; [|intro d'; simpl; rewrite IHd; simpl..].
+Qed.
+
+Lemma nb_digits_rev u : nb_digits (rev u) = nb_digits u.
+Proof. now unfold rev; rewrite nb_digits_revapp. Qed.
+
+Lemma nb_digits_nzhead u : nb_digits (nzhead u) <= nb_digits u.
+Proof. now induction u; [|apply le_S|..]. Qed.
+
+Lemma nb_digits_iter_D0 n d :
+  nb_digits (Nat.iter n D0 d) = n + nb_digits d.
+Proof. now induction n; simpl; [|rewrite IHn]. Qed.
+
+Fixpoint nth n u :=
+  match n with
+  | O =>
+    match u with
+    | Nil => Nil
+    | D0 d => D0 Nil
+    | D1 d => D1 Nil
+    | D2 d => D2 Nil
+    | D3 d => D3 Nil
+    | D4 d => D4 Nil
+    | D5 d => D5 Nil
+    | D6 d => D6 Nil
+    | D7 d => D7 Nil
+    | D8 d => D8 Nil
+    | D9 d => D9 Nil
+    | Da d => Da Nil
+    | Db d => Db Nil
+    | Dc d => Dc Nil
+    | Dd d => Dd Nil
+    | De d => De Nil
+    | Df d => Df Nil
+    end
+  | S n =>
+    match u with
+    | Nil => Nil
+    | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d
+    | Da d | Db d | Dc d | Dd d | De d | Df d =>
+      nth n d
+    end
+  end.
+
+Lemma nb_digits_nth n u : nb_digits (nth n u) <= 1.
+Proof.
+  revert u; induction n.
+  - now intro u; case u; [apply Nat.le_0_1|..].
+  - intro u; case u; [apply Nat.le_0_1|intro u'; apply IHn..].
+Qed.
+
+Lemma nth_revapp_r n d d' :
+  nb_digits d <= n ->
+  nth n (revapp d d') = nth (n - nb_digits d) d'.
+Proof.
+  revert d d'; induction n; intro d.
+  - now case d; intro d';
+      [case d'|intros d'' H; exfalso; revert H; apply Nat.nle_succ_0..].
+  - now induction d;
+      [intro d'; case d'|
+       intros d' H;
+       simpl revapp; rewrite IHd; [|now apply le_Sn_le];
+       rewrite Nat.sub_succ_l; [|now apply le_S_n];
+       simpl; rewrite <-(IHn _ _ (le_S_n _ _ H))..].
+Qed.
+
+Lemma nth_revapp_l n d d' :
+  n < nb_digits d ->
+  nth n (revapp d d') = nth (nb_digits d - n - 1) d.
+Proof.
+  revert d d'; induction n; intro d.
+  - rewrite Nat.sub_0_r.
+    now induction d;
+      [|intros d' _; simpl revapp;
+       revert IHd; case d; clear d; [|intro d..]; intro IHd;
+       [|rewrite IHd; [simpl nb_digits; rewrite (Nat.sub_succ_l _ (S _))|];
+         [|apply le_n_S, Nat.le_0_l..]..]..].
+  - now induction d;
+      [|intros d' H;
+        simpl revapp; simpl nb_digits;
+        simpl in H; generalize (lt_S_n _ _ H); clear H; intro H;
+        case (le_lt_eq_dec _ _ H); clear H; intro H;
+        [rewrite (IHd _ H), Nat.sub_succ_l;
+         [rewrite Nat.sub_succ_l; [|apply Nat.le_add_le_sub_r]|
+          apply le_Sn_le]|
+         rewrite nth_revapp_r; rewrite <-H;
+         [rewrite Nat.sub_succ, Nat.sub_succ_l; [rewrite !Nat.sub_diag|]|]]..].
+Qed.
+
+(** Normalization on little-endian numbers *)
+
+Fixpoint nztail d :=
+  match d with
+  | Nil => Nil
+  | D0 d => match nztail d with Nil => Nil | d' => D0 d' end
+  | D1 d => D1 (nztail d)
+  | D2 d => D2 (nztail d)
+  | D3 d => D3 (nztail d)
+  | D4 d => D4 (nztail d)
+  | D5 d => D5 (nztail d)
+  | D6 d => D6 (nztail d)
+  | D7 d => D7 (nztail d)
+  | D8 d => D8 (nztail d)
+  | D9 d => D9 (nztail d)
+  | Da d => Da (nztail d)
+  | Db d => Db (nztail d)
+  | Dc d => Dc (nztail d)
+  | Dd d => Dd (nztail d)
+  | De d => De (nztail d)
+  | Df d => Df (nztail d)
+  end.
+
+Definition lnorm d :=
+  match nztail d with
+  | Nil => zero
+  | d => d
+  end.
+
+Lemma nzhead_revapp_0 d d' : nztail d = Nil ->
+  nzhead (revapp d d') = nzhead d'.
+Proof.
+  revert d'. induction d; intros d' [=]; simpl; trivial.
+  destruct (nztail d); now rewrite IHd.
+Qed.
+
+Lemma nzhead_revapp d d' : nztail d <> Nil ->
+  nzhead (revapp d d') = revapp (nztail d) d'.
+Proof.
+  revert d'.
+  induction d; intros d' H; simpl in *;
+  try destruct (nztail d) eqn:E;
+  (now rewrite ?nzhead_revapp_0) || (now rewrite IHd).
+Qed.
+
+Lemma nzhead_rev d : nztail d <> Nil ->
+  nzhead (rev d) = rev (nztail d).
+Proof.
+  apply nzhead_revapp.
+Qed.
+
+Lemma rev_nztail_rev d :
+  rev (nztail (rev d)) = nzhead d.
+Proof.
+  destruct (uint_eq_dec (nztail (rev d)) Nil) as [H|H].
+  - rewrite H. unfold rev; simpl.
+    rewrite <- (rev_rev d). symmetry.
+    now apply nzhead_revapp_0.
+  - now rewrite <- nzhead_rev, rev_rev.
+Qed.
+
+Lemma nzhead_D0 u : nzhead (D0 u) = nzhead u.
+Proof. reflexivity. Qed.
+
+Lemma nzhead_iter_D0 n u : nzhead (Nat.iter n D0 u) = nzhead u.
+Proof. now induction n. Qed.
+
+Lemma revapp_nil_inv d d' : revapp d d' = Nil -> d = Nil /\ d' = Nil.
+Proof.
+  revert d'.
+  induction d; simpl; intros d' H; auto; now apply IHd in H.
+Qed.
+
+Lemma rev_nil_inv d : rev d = Nil -> d = Nil.
+Proof.
+  apply revapp_nil_inv.
+Qed.
+
+Lemma rev_lnorm_rev d :
+  rev (lnorm (rev d)) = unorm d.
+Proof.
+  unfold unorm, lnorm.
+  rewrite <- rev_nztail_rev.
+  destruct nztail; simpl; trivial;
+    destruct rev eqn:E; trivial; now apply rev_nil_inv in E.
+Qed.
+
+Lemma nzhead_nonzero d d' : nzhead d <> D0 d'.
+Proof.
+  induction d; easy.
+Qed.
+
+Lemma unorm_0 d : unorm d = zero <-> nzhead d = Nil.
+Proof.
+  unfold unorm. split.
+  - generalize (nzhead_nonzero d).
+    destruct nzhead; intros H [=]; trivial. now destruct (H u).
+  - now intros ->.
+Qed.
+
+Lemma unorm_nonnil d : unorm d <> Nil.
+Proof.
+  unfold unorm. now destruct nzhead.
+Qed.
+
+Lemma unorm_D0 u : unorm (D0 u) = unorm u.
+Proof. reflexivity. Qed.
+
+Lemma unorm_iter_D0 n u : unorm (Nat.iter n D0 u) = unorm u.
+Proof. now induction n. Qed.
+
+Lemma nb_digits_unorm u :
+  u <> Nil -> nb_digits (unorm u) <= nb_digits u.
+Proof.
+  case u; clear u; [now simpl|intro u..]; [|now simpl..].
+  intros _; unfold unorm.
+  case_eq (nzhead (D0 u)); [|now intros u' <-; apply nb_digits_nzhead..].
+  intros _; apply le_n_S, Nat.le_0_l.
+Qed.
+
+Lemma nzhead_invol d : nzhead (nzhead d) = nzhead d.
+Proof.
+  now induction d.
+Qed.
+
+Lemma nztail_invol d : nztail (nztail d) = nztail d.
+Proof.
+  rewrite <-(rev_rev (nztail _)), <-(rev_rev (nztail d)), <-(rev_rev d).
+  now rewrite !rev_nztail_rev, nzhead_invol.
+Qed.
+
+Lemma unorm_invol d : unorm (unorm d) = unorm d.
+Proof.
+  unfold unorm.
+  destruct (nzhead d) eqn:E; trivial.
+  destruct (nzhead_nonzero _ _ E).
+Qed.
+
+Lemma norm_invol d : norm (norm d) = norm d.
+Proof.
+  unfold norm.
+  destruct d.
+  - f_equal. apply unorm_invol.
+  - destruct (nzhead d) eqn:E; auto.
+    destruct (nzhead_nonzero _ _ E).
+Qed.
+
+Lemma nzhead_app_nzhead d d' :
+  nzhead (app (nzhead d) d') = nzhead (app d d').
+Proof.
+  unfold app.
+  rewrite <-(rev_nztail_rev d), rev_rev.
+  generalize (rev d); clear d; intro d.
+  generalize (nzhead_revapp_0 d d').
+  generalize (nzhead_revapp d d').
+  generalize (nzhead_revapp_0 (nztail d) d').
+  generalize (nzhead_revapp (nztail d) d').
+  rewrite nztail_invol.
+  now case nztail;
+    [intros _ H _ H'; rewrite (H eq_refl), (H' eq_refl)
+    |intros d'' H _ H' _; rewrite H; [rewrite H'|]..].
+Qed.
+
+Lemma unorm_app_unorm d d' :
+  unorm (app (unorm d) d') = unorm (app d d').
+Proof.
+  unfold unorm.
+  rewrite <-(nzhead_app_nzhead d d').
+  now case (nzhead d).
+Qed.
+
+Lemma norm_app_int_norm d d' :
+  unorm d' = zero ->
+  norm (app_int (norm d) d') = norm (app_int d d').
+Proof.
+  case d; clear d; intro d; simpl.
+  - now rewrite unorm_app_unorm.
+  - unfold app_int, app.
+    rewrite unorm_0; intro Hd'.
+    rewrite <-rev_nztail_rev.
+    generalize (nzhead_revapp (rev d) d').
+    generalize (nzhead_revapp_0 (rev d) d').
+    now case_eq (nztail (rev d));
+      [intros Hd'' H _; rewrite (H eq_refl); simpl;
+       unfold unorm; simpl; rewrite Hd'
+      |intros d'' Hd'' _ H; rewrite H; clear H; [|now simpl];
+       set (r := rev _);
+       set (m := match r with Nil => Pos zero | _ => _ end);
+       assert (H' : m = Neg r);
+       [now unfold m; case_eq r; unfold r;
+        [intro H''; generalize (rev_nil_inv _ H'')|..]
+       |rewrite H'; unfold r; clear m r H'];
+       unfold norm;
+       rewrite rev_rev, <-Hd'';
+       rewrite nzhead_revapp; rewrite nztail_invol; [|rewrite Hd'']..].
+Qed.
diff --git a/theories/Numbers/HexadecimalN.v b/theories/Numbers/HexadecimalN.v
new file mode 100644
index 0000000000..f333e2b7f6
--- /dev/null
+++ b/theories/Numbers/HexadecimalN.v
@@ -0,0 +1,107 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** * HexadecimalN
+
+    Proofs that conversions between hexadecimal numbers and [N]
+    are bijections *)
+
+Require Import Hexadecimal HexadecimalFacts HexadecimalPos PArith NArith.
+
+Module Unsigned.
+
+Lemma of_to (n:N) : N.of_hex_uint (N.to_hex_uint n) = n.
+Proof.
+  destruct n.
+  - reflexivity.
+  - apply HexadecimalPos.Unsigned.of_to.
+Qed.
+
+Lemma to_of (d:uint) : N.to_hex_uint (N.of_hex_uint d) = unorm d.
+Proof.
+  exact (HexadecimalPos.Unsigned.to_of d).
+Qed.
+
+Lemma to_uint_inj n n' : N.to_hex_uint n = N.to_hex_uint n' -> n = n'.
+Proof.
+  intros E. now rewrite <- (of_to n), <- (of_to n'), E.
+Qed.
+
+Lemma to_uint_surj d : exists p, N.to_hex_uint p = unorm d.
+Proof.
+  exists (N.of_hex_uint d). apply to_of.
+Qed.
+
+Lemma of_uint_norm d : N.of_hex_uint (unorm d) = N.of_hex_uint d.
+Proof.
+  now induction d.
+Qed.
+
+Lemma of_inj d d' :
+  N.of_hex_uint d = N.of_hex_uint d' -> unorm d = unorm d'.
+Proof.
+  intros. rewrite <- !to_of. now f_equal.
+Qed.
+
+Lemma of_iff d d' : N.of_hex_uint d = N.of_hex_uint d' <-> unorm d = unorm d'.
+Proof.
+  split. apply of_inj. intros E. rewrite <- of_uint_norm, E.
+  apply of_uint_norm.
+Qed.
+
+End Unsigned.
+
+(** Conversion from/to signed hexadecimal numbers *)
+
+Module Signed.
+
+Lemma of_to (n:N) : N.of_hex_int (N.to_hex_int n) = Some n.
+Proof.
+  unfold N.to_hex_int, N.of_hex_int, norm. f_equal.
+  rewrite Unsigned.of_uint_norm. apply Unsigned.of_to.
+Qed.
+
+Lemma to_of (d:int)(n:N) : N.of_hex_int d = Some n -> N.to_hex_int n = norm d.
+Proof.
+  unfold N.of_hex_int.
+  destruct (norm d) eqn:Hd; intros [= <-].
+  unfold N.to_hex_int. rewrite Unsigned.to_of. f_equal.
+  revert Hd; destruct d; simpl.
+  - intros [= <-]. apply unorm_invol.
+  - destruct (nzhead d); now intros [= <-].
+Qed.
+
+Lemma to_int_inj n n' : N.to_hex_int n = N.to_hex_int n' -> n = n'.
+Proof.
+  intro E.
+  assert (E' : Some n = Some n').
+  { now rewrite <- (of_to n), <- (of_to n'), E. }
+  now injection E'.
+Qed.
+
+Lemma to_int_pos_surj d : exists n, N.to_hex_int n = norm (Pos d).
+Proof.
+  exists (N.of_hex_uint d). unfold N.to_hex_int. now rewrite Unsigned.to_of.
+Qed.
+
+Lemma of_int_norm d : N.of_hex_int (norm d) = N.of_hex_int d.
+Proof.
+  unfold N.of_hex_int. now rewrite norm_invol.
+Qed.
+
+Lemma of_inj_pos d d' :
+  N.of_hex_int (Pos d) = N.of_hex_int (Pos d') -> unorm d = unorm d'.
+Proof.
+  unfold N.of_hex_int. simpl. intros [= H]. apply Unsigned.of_inj.
+  change Pos.of_hex_uint with N.of_hex_uint in H.
+  now rewrite <- Unsigned.of_uint_norm, H, Unsigned.of_uint_norm.
+Qed.
+
+End Signed.
diff --git a/theories/Numbers/HexadecimalNat.v b/theories/Numbers/HexadecimalNat.v
new file mode 100644
index 0000000000..b05184e821
--- /dev/null
+++ b/theories/Numbers/HexadecimalNat.v
@@ -0,0 +1,321 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** * HexadecimalNat
+
+    Proofs that conversions between hexadecimal numbers and [nat]
+    are bijections. *)
+
+Require Import Hexadecimal HexadecimalFacts Arith.
+
+Module Unsigned.
+
+(** A few helper functions used during proofs *)
+
+Definition hd d :=
+  match d with
+  | Nil => 0x0
+  | D0 _ => 0x0
+  | D1 _ => 0x1
+  | D2 _ => 0x2
+  | D3 _ => 0x3
+  | D4 _ => 0x4
+  | D5 _ => 0x5
+  | D6 _ => 0x6
+  | D7 _ => 0x7
+  | D8 _ => 0x8
+  | D9 _ => 0x9
+  | Da _ => 0xa
+  | Db _ => 0xb
+  | Dc _ => 0xc
+  | Dd _ => 0xd
+  | De _ => 0xe
+  | Df _ => 0xf
+  end.
+
+Definition tl d :=
+  match d with
+  | Nil => d
+  | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d
+  | Da d | Db d | Dc d | Dd d | De d | Df d => d
+  end.
+
+Fixpoint usize (d:uint) : nat :=
+  match d with
+  | Nil => 0
+  | D0 d => S (usize d)
+  | D1 d => S (usize d)
+  | D2 d => S (usize d)
+  | D3 d => S (usize d)
+  | D4 d => S (usize d)
+  | D5 d => S (usize d)
+  | D6 d => S (usize d)
+  | D7 d => S (usize d)
+  | D8 d => S (usize d)
+  | D9 d => S (usize d)
+  | Da d => S (usize d)
+  | Db d => S (usize d)
+  | Dc d => S (usize d)
+  | Dd d => S (usize d)
+  | De d => S (usize d)
+  | Df d => S (usize d)
+  end.
+
+(** A direct version of [to_little_uint], not tail-recursive *)
+Fixpoint to_lu n :=
+  match n with
+  | 0 => Hexadecimal.zero
+  | S n => Little.succ (to_lu n)
+  end.
+
+(** A direct version of [of_little_uint] *)
+Fixpoint of_lu (d:uint) : nat :=
+  match d with
+  | Nil => 0x0
+  | D0 d => 0x10 * of_lu d
+  | D1 d => 0x1 + 0x10 * of_lu d
+  | D2 d => 0x2 + 0x10 * of_lu d
+  | D3 d => 0x3 + 0x10 * of_lu d
+  | D4 d => 0x4 + 0x10 * of_lu d
+  | D5 d => 0x5 + 0x10 * of_lu d
+  | D6 d => 0x6 + 0x10 * of_lu d
+  | D7 d => 0x7 + 0x10 * of_lu d
+  | D8 d => 0x8 + 0x10 * of_lu d
+  | D9 d => 0x9 + 0x10 * of_lu d
+  | Da d => 0xa + 0x10 * of_lu d
+  | Db d => 0xb + 0x10 * of_lu d
+  | Dc d => 0xc + 0x10 * of_lu d
+  | Dd d => 0xd + 0x10 * of_lu d
+  | De d => 0xe + 0x10 * of_lu d
+  | Df d => 0xf + 0x10 * of_lu d
+  end.
+
+(** Properties of [to_lu] *)
+
+Lemma to_lu_succ n : to_lu (S n) = Little.succ (to_lu n).
+Proof.
+  reflexivity.
+Qed.
+
+Lemma to_little_uint_succ n d :
+  Nat.to_little_hex_uint n (Little.succ d) =
+    Little.succ (Nat.to_little_hex_uint n d).
+Proof.
+  revert d; induction n; simpl; trivial.
+Qed.
+
+Lemma to_lu_equiv n :
+  to_lu n = Nat.to_little_hex_uint n zero.
+Proof.
+  induction n; simpl; trivial.
+  now rewrite IHn, <- to_little_uint_succ.
+Qed.
+
+Lemma to_uint_alt n :
+  Nat.to_hex_uint n = rev (to_lu n).
+Proof.
+  unfold Nat.to_hex_uint. f_equal. symmetry. apply to_lu_equiv.
+Qed.
+
+(** Properties of [of_lu] *)
+
+Lemma of_lu_eqn d :
+  of_lu d = hd d + 0x10 * of_lu (tl d).
+Proof.
+  induction d; simpl; trivial.
+Qed.
+
+Ltac simpl_of_lu :=
+  match goal with
+  | |- context [ of_lu (?f ?x) ] =>
+    rewrite (of_lu_eqn (f x)); simpl hd; simpl tl
+  end.
+
+Lemma of_lu_succ d :
+  of_lu (Little.succ d) = S (of_lu d).
+Proof.
+  induction d; trivial.
+  simpl_of_lu. rewrite IHd. simpl_of_lu.
+  now rewrite Nat.mul_succ_r, <- (Nat.add_comm 0x10).
+Qed.
+
+Lemma of_to_lu n :
+  of_lu (to_lu n) = n.
+Proof.
+  induction n; simpl; trivial. rewrite of_lu_succ. now f_equal.
+Qed.
+
+Lemma of_lu_revapp d d' :
+  of_lu (revapp d d') =
+    of_lu (rev d) + of_lu d' * 0x10^usize d.
+Proof.
+  revert d'.
+  induction d; intro d'; simpl usize;
+  [ simpl; now rewrite Nat.mul_1_r | .. ];
+  unfold rev; simpl revapp; rewrite 2 IHd;
+  rewrite <- Nat.add_assoc; f_equal; simpl_of_lu; simpl of_lu;
+  rewrite Nat.pow_succ_r'; ring.
+Qed.
+
+Lemma of_uint_acc_spec n d :
+  Nat.of_hex_uint_acc d n = of_lu (rev d) + n * 0x10^usize d.
+Proof.
+  revert n. induction d; intros;
+  simpl Nat.of_hex_uint_acc; rewrite ?Nat.tail_mul_spec, ?IHd;
+  simpl rev; simpl usize; rewrite ?Nat.pow_succ_r';
+  [ simpl; now rewrite Nat.mul_1_r | .. ];
+  unfold rev at 2; simpl revapp; rewrite of_lu_revapp;
+  simpl of_lu; ring.
+Qed.
+
+Lemma of_uint_alt d : Nat.of_hex_uint d = of_lu (rev d).
+Proof.
+  unfold Nat.of_hex_uint. now rewrite of_uint_acc_spec.
+Qed.
+
+(** First main bijection result *)
+
+Lemma of_to (n:nat) : Nat.of_hex_uint (Nat.to_hex_uint n) = n.
+Proof.
+  rewrite to_uint_alt, of_uint_alt, rev_rev. apply of_to_lu.
+Qed.
+
+(** The other direction *)
+
+Lemma to_lu_sixteenfold n : n<>0 ->
+  to_lu (0x10 * n) = D0 (to_lu n).
+Proof.
+  induction n.
+  - simpl. now destruct 1.
+  - intros _.
+    destruct (Nat.eq_dec n 0) as [->|H]; simpl; trivial.
+    rewrite !Nat.add_succ_r.
+    simpl in *. rewrite (IHn H). now destruct (to_lu n).
+Qed.
+
+Lemma of_lu_0 d : of_lu d = 0 <-> nztail d = Nil.
+Proof.
+  induction d; try simpl_of_lu; try easy.
+  rewrite Nat.add_0_l.
+  split; intros H.
+  - apply Nat.eq_mul_0_r in H; auto.
+    rewrite IHd in H. simpl. now rewrite H.
+  - simpl in H. destruct (nztail d); try discriminate.
+    now destruct IHd as [_ ->].
+Qed.
+
+Lemma to_of_lu_sixteenfold d :
+  to_lu (of_lu d) = lnorm d ->
+  to_lu (0x10 * of_lu d) = lnorm (D0 d).
+Proof.
+  intro IH.
+  destruct (Nat.eq_dec (of_lu d) 0) as [H|H].
+  - rewrite H. simpl. rewrite of_lu_0 in H.
+    unfold lnorm. simpl. now rewrite H.
+  - rewrite (to_lu_sixteenfold _ H), IH.
+    rewrite of_lu_0 in H.
+    unfold lnorm. simpl. now destruct (nztail d).
+Qed.
+
+Lemma to_of_lu d : to_lu (of_lu d) = lnorm d.
+Proof.
+  induction d; [ reflexivity | .. ];
+  simpl_of_lu;
+  rewrite ?Nat.add_succ_l, Nat.add_0_l, ?to_lu_succ, to_of_lu_sixteenfold
+   by assumption;
+  unfold lnorm; simpl; now destruct nztail.
+Qed.
+
+(** Second bijection result *)
+
+Lemma to_of (d:uint) : Nat.to_hex_uint (Nat.of_hex_uint d) = unorm d.
+Proof.
+  rewrite to_uint_alt, of_uint_alt, to_of_lu.
+  apply rev_lnorm_rev.
+Qed.
+
+(** Some consequences *)
+
+Lemma to_uint_inj n n' : Nat.to_hex_uint n = Nat.to_hex_uint n' -> n = n'.
+Proof.
+  intro EQ.
+  now rewrite <- (of_to n), <- (of_to n'), EQ.
+Qed.
+
+Lemma to_uint_surj d : exists n, Nat.to_hex_uint n = unorm d.
+Proof.
+  exists (Nat.of_hex_uint d). apply to_of.
+Qed.
+
+Lemma of_uint_norm d : Nat.of_hex_uint (unorm d) = Nat.of_hex_uint d.
+Proof.
+  unfold Nat.of_hex_uint. now induction d.
+Qed.
+
+Lemma of_inj d d' :
+  Nat.of_hex_uint d = Nat.of_hex_uint d' -> unorm d = unorm d'.
+Proof.
+  intros. rewrite <- !to_of. now f_equal.
+Qed.
+
+Lemma of_iff d d' : Nat.of_hex_uint d = Nat.of_hex_uint d' <-> unorm d = unorm d'.
+Proof.
+  split. apply of_inj. intros E. rewrite <- of_uint_norm, E.
+  apply of_uint_norm.
+Qed.
+
+End Unsigned.
+
+(** Conversion from/to signed hexadecimal numbers *)
+
+Module Signed.
+
+Lemma of_to (n:nat) : Nat.of_hex_int (Nat.to_hex_int n) = Some n.
+Proof.
+  unfold Nat.to_hex_int, Nat.of_hex_int, norm. f_equal.
+  rewrite Unsigned.of_uint_norm. apply Unsigned.of_to.
+Qed.
+
+Lemma to_of (d:int)(n:nat) : Nat.of_hex_int d = Some n -> Nat.to_hex_int n = norm d.
+Proof.
+  unfold Nat.of_hex_int.
+  destruct (norm d) eqn:Hd; intros [= <-].
+  unfold Nat.to_hex_int. rewrite Unsigned.to_of. f_equal.
+  revert Hd; destruct d; simpl.
+  - intros [= <-]. apply unorm_invol.
+  - destruct (nzhead d); now intros [= <-].
+Qed.
+
+Lemma to_int_inj n n' : Nat.to_hex_int n = Nat.to_hex_int n' -> n = n'.
+Proof.
+  intro E.
+  assert (E' : Some n = Some n').
+  { now rewrite <- (of_to n), <- (of_to n'), E. }
+  now injection E'.
+Qed.
+
+Lemma to_int_pos_surj d : exists n, Nat.to_hex_int n = norm (Pos d).
+Proof.
+  exists (Nat.of_hex_uint d). unfold Nat.to_hex_int. now rewrite Unsigned.to_of.
+Qed.
+
+Lemma of_int_norm d : Nat.of_hex_int (norm d) = Nat.of_hex_int d.
+Proof.
+  unfold Nat.of_hex_int. now rewrite norm_invol.
+Qed.
+
+Lemma of_inj_pos d d' :
+  Nat.of_hex_int (Pos d) = Nat.of_hex_int (Pos d') -> unorm d = unorm d'.
+Proof.
+  unfold Nat.of_hex_int. simpl. intros [= H]. apply Unsigned.of_inj.
+  now rewrite <- Unsigned.of_uint_norm, H, Unsigned.of_uint_norm.
+Qed.
+
+End Signed.
diff --git a/theories/Numbers/HexadecimalPos.v b/theories/Numbers/HexadecimalPos.v
new file mode 100644
index 0000000000..47f6d983b7
--- /dev/null
+++ b/theories/Numbers/HexadecimalPos.v
@@ -0,0 +1,446 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** * HexadecimalPos
+
+    Proofs that conversions between hexadecimal numbers and [positive]
+    are bijections. *)
+
+Require Import Hexadecimal HexadecimalFacts PArith NArith.
+
+Module Unsigned.
+
+Local Open Scope N.
+
+(** A direct version of [of_little_uint] *)
+Fixpoint of_lu (d:uint) : N :=
+  match d with
+  | Nil => 0
+  | D0 d => 0x10 * of_lu d
+  | D1 d => 0x1 + 0x10 * of_lu d
+  | D2 d => 0x2 + 0x10 * of_lu d
+  | D3 d => 0x3 + 0x10 * of_lu d
+  | D4 d => 0x4 + 0x10 * of_lu d
+  | D5 d => 0x5 + 0x10 * of_lu d
+  | D6 d => 0x6 + 0x10 * of_lu d
+  | D7 d => 0x7 + 0x10 * of_lu d
+  | D8 d => 0x8 + 0x10 * of_lu d
+  | D9 d => 0x9 + 0x10 * of_lu d
+  | Da d => 0xa + 0x10 * of_lu d
+  | Db d => 0xb + 0x10 * of_lu d
+  | Dc d => 0xc + 0x10 * of_lu d
+  | Dd d => 0xd + 0x10 * of_lu d
+  | De d => 0xe + 0x10 * of_lu d
+  | Df d => 0xf + 0x10 * of_lu d
+  end.
+
+Definition hd d :=
+  match d with
+  | Nil => 0x0
+  | D0 _ => 0x0
+  | D1 _ => 0x1
+  | D2 _ => 0x2
+  | D3 _ => 0x3
+  | D4 _ => 0x4
+  | D5 _ => 0x5
+  | D6 _ => 0x6
+  | D7 _ => 0x7
+  | D8 _ => 0x8
+  | D9 _ => 0x9
+  | Da _ => 0xa
+  | Db _ => 0xb
+  | Dc _ => 0xc
+  | Dd _ => 0xd
+  | De _ => 0xe
+  | Df _ => 0xf
+  end.
+
+Definition tl d :=
+  match d with
+  | Nil => d
+  | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d
+  | Da d | Db d | Dc d | Dd d | De d | Df d => d
+  end.
+
+Lemma of_lu_eqn d :
+  of_lu d = hd d + 0x10 * (of_lu (tl d)).
+Proof.
+  induction d; simpl; trivial.
+Qed.
+
+Ltac simpl_of_lu :=
+  match goal with
+  | |- context [ of_lu (?f ?x) ] =>
+    rewrite (of_lu_eqn (f x)); simpl hd; simpl tl
+  end.
+
+Fixpoint usize (d:uint) : N :=
+  match d with
+  | Nil => 0
+  | D0 d => N.succ (usize d)
+  | D1 d => N.succ (usize d)
+  | D2 d => N.succ (usize d)
+  | D3 d => N.succ (usize d)
+  | D4 d => N.succ (usize d)
+  | D5 d => N.succ (usize d)
+  | D6 d => N.succ (usize d)
+  | D7 d => N.succ (usize d)
+  | D8 d => N.succ (usize d)
+  | D9 d => N.succ (usize d)
+  | Da d => N.succ (usize d)
+  | Db d => N.succ (usize d)
+  | Dc d => N.succ (usize d)
+  | Dd d => N.succ (usize d)
+  | De d => N.succ (usize d)
+  | Df d => N.succ (usize d)
+  end.
+
+Lemma of_lu_revapp d d' :
+  of_lu (revapp d d') =
+    of_lu (rev d) + of_lu d' * 0x10^usize d.
+Proof.
+  revert d'.
+  induction d; simpl; intro d'; [ now rewrite N.mul_1_r | .. ];
+  unfold rev; simpl revapp; rewrite 2 IHd;
+  rewrite <- N.add_assoc; f_equal; simpl_of_lu; simpl of_lu;
+  rewrite N.pow_succ_r'; ring.
+Qed.
+
+Definition Nadd n p :=
+  match n with
+  | N0 => p
+  | Npos p0 => (p0+p)%positive
+  end.
+
+Lemma Nadd_simpl n p q : Npos (Nadd n (p * q)) = n + Npos p * Npos q.
+Proof.
+  now destruct n.
+Qed.
+
+Lemma of_uint_acc_eqn d acc : d<>Nil ->
+  Pos.of_hex_uint_acc d acc = Pos.of_hex_uint_acc (tl d) (Nadd (hd d) (0x10*acc)).
+Proof.
+  destruct d; simpl; trivial. now destruct 1.
+Qed.
+
+Lemma of_uint_acc_rev d acc :
+  Npos (Pos.of_hex_uint_acc d acc) =
+    of_lu (rev d) + (Npos acc) * 0x10^usize d.
+Proof.
+  revert acc.
+  induction d; intros; simpl usize;
+  [ simpl; now rewrite Pos.mul_1_r | .. ];
+  rewrite N.pow_succ_r';
+  unfold rev; simpl revapp; try rewrite of_lu_revapp; simpl of_lu;
+  rewrite of_uint_acc_eqn by easy; simpl tl; simpl hd;
+  rewrite IHd, Nadd_simpl; ring.
+Qed.
+
+Lemma of_uint_alt d : Pos.of_hex_uint d = of_lu (rev d).
+Proof.
+  induction d; simpl; trivial; unfold rev; simpl revapp;
+  rewrite of_lu_revapp; simpl of_lu; try apply of_uint_acc_rev.
+  rewrite IHd. ring.
+Qed.
+
+Lemma of_lu_rev d : Pos.of_hex_uint (rev d) = of_lu d.
+Proof.
+  rewrite of_uint_alt. now rewrite rev_rev.
+Qed.
+
+Lemma of_lu_double_gen d :
+  of_lu (Little.double d) = N.double (of_lu d) /\
+  of_lu (Little.succ_double d) = N.succ_double (of_lu d).
+Proof.
+  rewrite N.double_spec, N.succ_double_spec.
+  induction d; try destruct IHd as (IH1,IH2);
+  simpl Little.double; simpl Little.succ_double;
+  repeat (simpl_of_lu; rewrite ?IH1, ?IH2); split; reflexivity || ring.
+Qed.
+
+Lemma of_lu_double d :
+  of_lu (Little.double d) = N.double (of_lu d).
+Proof.
+  apply of_lu_double_gen.
+Qed.
+
+Lemma of_lu_succ_double d :
+  of_lu (Little.succ_double d) = N.succ_double (of_lu d).
+Proof.
+  apply of_lu_double_gen.
+Qed.
+
+(** First bijection result *)
+
+Lemma of_to (p:positive) : Pos.of_hex_uint (Pos.to_hex_uint p) = Npos p.
+Proof.
+  unfold Pos.to_hex_uint.
+  rewrite of_lu_rev.
+  induction p; simpl; trivial.
+  - now rewrite of_lu_succ_double, IHp.
+  - now rewrite of_lu_double, IHp.
+Qed.
+
+(** The other direction *)
+
+Definition to_lu n :=
+  match n with
+  | N0 => Hexadecimal.zero
+  | Npos p => Pos.to_little_hex_uint p
+  end.
+
+Lemma succ_double_alt d :
+  Little.succ_double d = Little.succ (Little.double d).
+Proof.
+  now induction d.
+Qed.
+
+Lemma double_succ d :
+  Little.double (Little.succ d) =
+  Little.succ (Little.succ_double d).
+Proof.
+  induction d; simpl; f_equal; auto using succ_double_alt.
+Qed.
+
+Lemma to_lu_succ n :
+  to_lu (N.succ n) = Little.succ (to_lu n).
+Proof.
+  destruct n; simpl; trivial.
+  induction p; simpl; rewrite ?IHp;
+    auto using succ_double_alt, double_succ.
+Qed.
+
+Lemma nat_iter_S n {A} (f:A->A) i :
+  Nat.iter (S n) f i = f (Nat.iter n f i).
+Proof.
+  reflexivity.
+Qed.
+
+Lemma nat_iter_0 {A} (f:A->A) i : Nat.iter 0 f i = i.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma to_lhex_tenfold p :
+  to_lu (0x10 * Npos p) = D0 (to_lu (Npos p)).
+Proof.
+  induction p using Pos.peano_rect.
+  - trivial.
+  - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)).
+    rewrite N.mul_succ_r.
+    change 0x10 at 2 with (Nat.iter 0x10%nat N.succ 0).
+    rewrite ?nat_iter_S, nat_iter_0.
+    rewrite !N.add_succ_r, N.add_0_r, !to_lu_succ, IHp.
+    destruct (to_lu (N.pos p)); simpl; auto.
+Qed.
+
+Lemma of_lu_0 d : of_lu d = 0 <-> nztail d = Nil.
+Proof.
+  induction d; try simpl_of_lu; split; trivial; try discriminate;
+  try (intros H; now apply N.eq_add_0 in H).
+  - rewrite N.add_0_l. intros H.
+    apply N.eq_mul_0_r in H; [|easy]. rewrite IHd in H.
+    simpl. now rewrite H.
+  - simpl. destruct (nztail d); try discriminate.
+    now destruct IHd as [_ ->].
+Qed.
+
+Lemma to_of_lu_tenfold d :
+  to_lu (of_lu d) = lnorm d ->
+  to_lu (0x10 * of_lu d) = lnorm (D0 d).
+Proof.
+  intro IH.
+  destruct (N.eq_dec (of_lu d) 0) as [H|H].
+  - rewrite H. simpl. rewrite of_lu_0 in H.
+    unfold lnorm. simpl. now rewrite H.
+  - destruct (of_lu d) eqn:Eq; [easy| ].
+    rewrite to_lhex_tenfold; auto. rewrite IH.
+    rewrite <- Eq in H. rewrite of_lu_0 in H.
+    unfold lnorm. simpl. now destruct (nztail d).
+Qed.
+
+Lemma Nadd_alt n m : n + m = Nat.iter (N.to_nat n) N.succ m.
+Proof.
+  destruct n. trivial.
+  induction p using Pos.peano_rect.
+  - now rewrite N.add_1_l.
+  - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)).
+    now rewrite N.add_succ_l, IHp, N2Nat.inj_succ.
+Qed.
+
+Ltac simpl_to_nat := simpl N.to_nat; unfold Pos.to_nat; simpl Pos.iter_op.
+
+Lemma to_of_lu d : to_lu (of_lu d) = lnorm d.
+Proof.
+  induction d; [reflexivity|..];
+  simpl_of_lu; rewrite Nadd_alt; simpl_to_nat;
+  rewrite ?nat_iter_S, nat_iter_0, ?to_lu_succ, to_of_lu_tenfold by assumption;
+  unfold lnorm; simpl; destruct nztail; auto.
+Qed.
+
+(** Second bijection result *)
+
+Lemma to_of (d:uint) : N.to_hex_uint (Pos.of_hex_uint d) = unorm d.
+Proof.
+  rewrite of_uint_alt.
+  unfold N.to_hex_uint, Pos.to_hex_uint.
+  destruct (of_lu (rev d)) eqn:H.
+  - rewrite of_lu_0 in H. rewrite <- rev_lnorm_rev.
+    unfold lnorm. now rewrite H.
+  - change (Pos.to_little_hex_uint p) with (to_lu (N.pos p)).
+    rewrite <- H. rewrite to_of_lu. apply rev_lnorm_rev.
+Qed.
+
+(** Some consequences *)
+
+Lemma to_uint_nonzero p : Pos.to_hex_uint p <> zero.
+Proof.
+  intro E. generalize (of_to p). now rewrite E.
+Qed.
+
+Lemma to_uint_nonnil p : Pos.to_hex_uint p <> Nil.
+Proof.
+  intros E. generalize (of_to p). now rewrite E.
+Qed.
+
+Lemma to_uint_inj p p' : Pos.to_hex_uint p = Pos.to_hex_uint p' -> p = p'.
+Proof.
+  intro E.
+  assert (E' : N.pos p = N.pos p').
+  { now rewrite <- (of_to p), <- (of_to p'), E. }
+  now injection E'.
+Qed.
+
+Lemma to_uint_pos_surj d :
+  unorm d<>zero -> exists p, Pos.to_hex_uint p = unorm d.
+Proof.
+  intros.
+  destruct (Pos.of_hex_uint d) eqn:E.
+  - destruct H. generalize (to_of d). now rewrite E.
+  - exists p. generalize (to_of d). now rewrite E.
+Qed.
+
+Lemma of_uint_norm d : Pos.of_hex_uint (unorm d) = Pos.of_hex_uint d.
+Proof.
+  now induction d.
+Qed.
+
+Lemma of_inj d d' :
+  Pos.of_hex_uint d = Pos.of_hex_uint d' -> unorm d = unorm d'.
+Proof.
+  intros. rewrite <- !to_of. now f_equal.
+Qed.
+
+Lemma of_iff d d' : Pos.of_hex_uint d = Pos.of_hex_uint d' <-> unorm d = unorm d'.
+Proof.
+  split. apply of_inj. intros E. rewrite <- of_uint_norm, E.
+  apply of_uint_norm.
+Qed.
+
+(* various lemmas *)
+
+Lemma nztail_to_hex_uint p :
+  let (h, n) := Hexadecimal.nztail (Pos.to_hex_uint p) in
+  Npos p = Pos.of_hex_uint h * 0x10^(N.of_nat n).
+Proof.
+  rewrite <-(of_to p), <-(rev_rev (Pos.to_hex_uint p)), of_lu_rev.
+  unfold Hexadecimal.nztail.
+  rewrite rev_rev.
+  induction (rev (Pos.to_hex_uint p)); [reflexivity| |
+    now simpl N.of_nat; simpl N.pow; rewrite N.mul_1_r, of_lu_rev..].
+  revert IHu.
+  set (t := _ u); case t; clear t; intros u0 n H.
+  rewrite of_lu_eqn; unfold hd, tl.
+  rewrite N.add_0_l, H, Nat2N.inj_succ, N.pow_succ_r'; ring.
+Qed.
+
+Definition double d := rev (Little.double (rev d)).
+
+Lemma double_unorm d : double (unorm d) = unorm (double d).
+Proof.
+  unfold double.
+  rewrite <-!rev_lnorm_rev, !rev_rev, <-!to_of_lu, of_lu_double.
+  now case of_lu; [now simpl|]; intro p; induction p.
+Qed.
+
+Lemma double_nzhead d : double (nzhead d) = nzhead (double d).
+Proof.
+  unfold double.
+  rewrite <-!rev_nztail_rev, !rev_rev.
+  apply f_equal; generalize (rev d); clear d; intro d.
+  cut (Little.double (nztail d) = nztail (Little.double d)
+       /\ Little.succ_double (nztail d) = nztail (Little.succ_double d)).
+  { now simpl. }
+  now induction d;
+    [|split; simpl; rewrite <-?(proj1 IHd), <-?(proj2 IHd); case nztail..].
+Qed.
+
+Lemma of_hex_uint_double d :
+  Pos.of_hex_uint (double d) = N.double (Pos.of_hex_uint d).
+Proof.
+  now unfold double; rewrite of_lu_rev, of_lu_double, <-of_lu_rev, rev_rev.
+Qed.
+
+End Unsigned.
+
+(** Conversion from/to signed decimal numbers *)
+
+Module Signed.
+
+Lemma of_to (p:positive) : Pos.of_hex_int (Pos.to_hex_int p) = Some p.
+Proof.
+  unfold Pos.to_hex_int, Pos.of_hex_int, norm.
+  now rewrite Unsigned.of_to.
+Qed.
+
+Lemma to_of (d:int)(p:positive) :
+  Pos.of_hex_int d = Some p -> Pos.to_hex_int p = norm d.
+Proof.
+  unfold Pos.of_hex_int.
+  destruct d; [ | intros [=]].
+  simpl norm. rewrite <- Unsigned.to_of.
+  destruct (Pos.of_hex_uint d); now intros [= <-].
+Qed.
+
+Lemma to_int_inj p p' : Pos.to_hex_int p = Pos.to_hex_int p' -> p = p'.
+Proof.
+  intro E.
+  assert (E' : Some p = Some p').
+  { now rewrite <- (of_to p), <- (of_to p'), E. }
+  now injection E'.
+Qed.
+
+Lemma to_int_pos_surj d :
+  unorm d <> zero -> exists p, Pos.to_hex_int p = norm (Pos d).
+Proof.
+  simpl. unfold Pos.to_hex_int. intros H.
+  destruct (Unsigned.to_uint_pos_surj d H) as (p,Hp).
+  exists p. now f_equal.
+Qed.
+
+Lemma of_int_norm d : Pos.of_hex_int (norm d) = Pos.of_hex_int d.
+Proof.
+  unfold Pos.of_int.
+  destruct d.
+  - simpl. now rewrite Unsigned.of_uint_norm.
+  - simpl. now destruct (nzhead d) eqn:H.
+Qed.
+
+Lemma of_inj_pos d d' :
+  Pos.of_hex_int (Pos d) = Pos.of_hex_int (Pos d') -> unorm d = unorm d'.
+Proof.
+  unfold Pos.of_hex_int.
+  destruct (Pos.of_hex_uint d) eqn:Hd, (Pos.of_hex_uint d') eqn:Hd';
+    intros [=].
+  - apply Unsigned.of_inj; now rewrite Hd, Hd'.
+  - apply Unsigned.of_inj; rewrite Hd, Hd'; now f_equal.
+Qed.
+
+End Signed.
diff --git a/theories/Numbers/HexadecimalQ.v b/theories/Numbers/HexadecimalQ.v
new file mode 100644
index 0000000000..9bf43ceb88
--- /dev/null
+++ b/theories/Numbers/HexadecimalQ.v
@@ -0,0 +1,533 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** * HexadecimalQ
+
+    Proofs that conversions between hexadecimal numbers and [Q]
+    are bijections. *)
+
+Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ.
+Require Import Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN HexadecimalZ QArith.
+
+Lemma of_to (q:Q) : forall d, to_hexadecimal q = Some d -> of_hexadecimal d = q.
+Proof.
+  cut (match to_hexadecimal q with None => True | Some d => of_hexadecimal d = q end).
+  { now case to_hexadecimal; [intros d <- d' Hd'; injection Hd'; intros ->|]. }
+  destruct q as (num, den).
+  unfold to_hexadecimal; simpl Qnum; simpl Qden.
+  generalize (HexadecimalPos.Unsigned.nztail_to_hex_uint den).
+  case Hexadecimal.nztail; intros u n.
+  change 16%N with (2^4)%N; rewrite <-N.pow_mul_r.
+  change 4%N with (N.of_nat 4); rewrite <-Nnat.Nat2N.inj_mul.
+  change 4%Z with (Z.of_nat 4); rewrite <-Nat2Z.inj_mul.
+  case u; clear u; try (intros; exact I); [| | |]; intro u;
+    (case u; clear u; [|intros; exact I..]).
+  - unfold Pos.of_hex_uint, Pos.of_hex_uint_acc; rewrite N.mul_1_l.
+    case n.
+    + unfold of_hexadecimal, app_int, app, Z.to_hex_int; simpl.
+      intro H; inversion H as (H1); clear H H1.
+      case num; [reflexivity|intro pnum; fold (rev (rev (Pos.to_hex_uint pnum)))..].
+      * rewrite rev_rev; simpl.
+        now unfold Z.of_hex_uint; rewrite HexadecimalPos.Unsigned.of_to.
+      * rewrite rev_rev; simpl.
+      now unfold Z.of_hex_uint; rewrite HexadecimalPos.Unsigned.of_to.
+    + clear n; intros n.
+      intro H; injection H; intros ->; clear H.
+      unfold of_hexadecimal.
+      rewrite DecimalZ.of_to.
+      simpl nb_digits; rewrite Nat2Z.inj_0, Z.mul_0_r, Z.sub_0_r.
+      now apply f_equal2; [rewrite app_int_nil_r, of_to|].
+  - unfold Pos.of_hex_uint, Pos.of_hex_uint_acc.
+    rewrite <-N.pow_succ_r', <-Nnat.Nat2N.inj_succ.
+    intro H; injection H; intros ->; clear H.
+    fold (4 * n)%nat.
+    change 1%Z with (Z.of_nat 1); rewrite <-Znat.Nat2Z.inj_add.
+    unfold of_hexadecimal.
+    rewrite DecimalZ.of_to.
+    simpl nb_digits; rewrite Nat2Z.inj_0, Z.mul_0_r, Z.sub_0_r.
+    now apply f_equal2; [rewrite app_int_nil_r, of_to|].
+  - change 2%Z with (Z.of_nat 2); rewrite <-Znat.Nat2Z.inj_add.
+    unfold Pos.of_hex_uint, Pos.of_hex_uint_acc.
+    change 4%N with (2^2)%N; rewrite <-N.pow_add_r.
+    change 2%N with (N.of_nat 2); rewrite <-Nnat.Nat2N.inj_add.
+    intro H; injection H; intros ->; clear H.
+    fold (4 * n)%nat.
+    unfold of_hexadecimal.
+    rewrite DecimalZ.of_to.
+    simpl nb_digits; rewrite Nat2Z.inj_0, Z.mul_0_r, Z.sub_0_r.
+    now apply f_equal2; [rewrite app_int_nil_r, of_to|].
+  - change 3%Z with (Z.of_nat 3); rewrite <-Znat.Nat2Z.inj_add.
+    unfold Pos.of_hex_uint, Pos.of_hex_uint_acc.
+    change 8%N with (2^3)%N; rewrite <-N.pow_add_r.
+    change 3%N with (N.of_nat 3); rewrite <-Nnat.Nat2N.inj_add.
+    intro H; injection H; intros ->; clear H.
+    fold (4 * n)%nat.
+    unfold of_hexadecimal.
+    rewrite DecimalZ.of_to.
+    simpl nb_digits; rewrite Nat2Z.inj_0, Z.mul_0_r, Z.sub_0_r.
+    now apply f_equal2; [rewrite app_int_nil_r, of_to|].
+Qed.
+
+(* normalize without fractional part, for instance norme 0x1.2p-1 is 0x12e-5 *)
+Definition hnorme (d:hexadecimal) : hexadecimal :=
+  let '(i, f, e) :=
+    match d with
+    | Hexadecimal i f => (i, f, Decimal.Pos Decimal.Nil)
+    | HexadecimalExp i f e => (i, f, e)
+    end in
+  let i := norm (app_int i f) in
+  let e := (Z.of_int e - 4 * Z.of_nat (nb_digits f))%Z in
+  match e with
+  | Z0 => Hexadecimal i Nil
+  | Zpos e => Hexadecimal (Pos.iter double i e) Nil
+  | Zneg _ => HexadecimalExp i Nil (Decimal.norm (Z.to_int e))
+  end.
+
+Lemma hnorme_spec d :
+  match hnorme d with
+  | Hexadecimal i Nil => i = norm i
+  | HexadecimalExp i Nil e =>
+    i = norm i /\ e = Decimal.norm e /\ e <> Decimal.Pos Decimal.zero
+  | _ => False
+  end.
+Proof.
+  case d; clear d; intros i f; [|intro e]; unfold hnorme; simpl.
+  - case_eq (nb_digits f); [now simpl; rewrite norm_invol|]; intros nf Hnf.
+    split; [now simpl; rewrite norm_invol|].
+    unfold Z.of_nat.
+    now rewrite <-!DecimalZ.to_of, !DecimalZ.of_to.
+  - set (e' := (_ - _)%Z).
+    case_eq e'; [|intro pe'..]; intro He'.
+    + now rewrite norm_invol.
+    + rewrite Pos2Nat.inj_iter.
+      set (ne' := Pos.to_nat pe').
+      fold (Nat.iter ne' double (norm (app_int i f))).
+      induction ne'; [now simpl; rewrite norm_invol|].
+      now rewrite Unsigned.nat_iter_S, <-double_norm, IHne', norm_invol.
+    + split; [now rewrite norm_invol|].
+      split; [now rewrite DecimalFacts.norm_invol|].
+      rewrite <-DecimalZ.to_of, DecimalZ.of_to.
+      change (Decimal.Pos _) with (Z.to_int 0).
+      now intro H; generalize (DecimalZ.to_int_inj _ _ H).
+Qed.
+
+Lemma hnorme_invol d : hnorme (hnorme d) = hnorme d.
+Proof.
+  case d; clear d; intros i f; [|intro e]; unfold hnorme; simpl.
+  - case_eq (nb_digits f); [now simpl; rewrite app_int_nil_r, norm_invol|].
+    intros nf Hnf.
+    unfold Z.of_nat.
+    simpl.
+    set (pnf := Pos.to_uint _).
+    set (nz := Decimal.nzhead pnf).
+    assert (Hnz : nz <> Decimal.Nil).
+    { unfold nz, pnf.
+      rewrite <-DecimalFacts.unorm_0.
+      rewrite <-DecimalPos.Unsigned.to_of.
+      rewrite DecimalPos.Unsigned.of_to.
+      change Decimal.zero with (N.to_uint 0).
+      now intro H; generalize (DecimalN.Unsigned.to_uint_inj _ _ H). }
+    set (m := match nz with Decimal.Nil => _ | _ => _ end).
+    assert (Hm : m = (Decimal.Neg (Decimal.unorm pnf))).
+    { now revert Hnz; unfold m, nz, Decimal.unorm; fold nz; case nz. }
+    rewrite Hm; unfold pnf.
+    rewrite <-DecimalPos.Unsigned.to_of, DecimalPos.Unsigned.of_to.
+    simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to.
+    rewrite Z.sub_0_r; simpl.
+    fold pnf; fold nz; fold m; rewrite Hm; unfold pnf.
+    rewrite <-DecimalPos.Unsigned.to_of, DecimalPos.Unsigned.of_to.
+    now rewrite app_int_nil_r, norm_invol.
+  - set (e' := (_ - _)%Z).
+    case_eq e'; [|intro pe'..]; intro Hpe'.
+    + now simpl; rewrite app_int_nil_r, norm_invol.
+    + simpl; rewrite app_int_nil_r.
+      apply f_equal2; [|reflexivity].
+      rewrite Pos2Nat.inj_iter.
+      set (ne' := Pos.to_nat pe').
+      fold (Nat.iter ne' double (norm (app_int i f))).
+      induction ne'; [now simpl; rewrite norm_invol|].
+      now rewrite Unsigned.nat_iter_S, <-double_norm, IHne'.
+    + rewrite <-DecimalZ.to_of, !DecimalZ.of_to; simpl.
+      rewrite app_int_nil_r, norm_invol.
+      set (pnf := Pos.to_uint _).
+      set (nz := Decimal.nzhead pnf).
+      assert (Hnz : nz <> Decimal.Nil).
+      { unfold nz, pnf.
+        rewrite <-DecimalFacts.unorm_0.
+        rewrite <-DecimalPos.Unsigned.to_of.
+        rewrite DecimalPos.Unsigned.of_to.
+        change Decimal.zero with (N.to_uint 0).
+        now intro H; generalize (DecimalN.Unsigned.to_uint_inj _ _ H). }
+      set (m := match nz with Decimal.Nil => _ | _ => _ end).
+      assert (Hm : m = (Decimal.Neg (Decimal.unorm pnf))).
+      { now revert Hnz; unfold m, nz, Decimal.unorm; fold nz; case nz. }
+      rewrite Hm; unfold pnf.
+      now rewrite <-DecimalPos.Unsigned.to_of, DecimalPos.Unsigned.of_to.
+Qed.
+
+Lemma to_of (d:hexadecimal) :
+  to_hexadecimal (of_hexadecimal d) = Some (hnorme d).
+Proof.
+  unfold to_hexadecimal.
+  pose (t10 := fun y => (y~0~0~0~0)%positive).
+  assert (H : exists h e_den,
+             Hexadecimal.nztail (Pos.to_hex_uint (Qden (of_hexadecimal d)))
+             = (h, e_den)
+             /\ (h = D1 Nil \/ h = D2 Nil \/ h = D4 Nil \/ h = D8 Nil)).
+  { assert (H : forall p,
+               Hexadecimal.nztail (Pos.to_hex_uint (Pos.iter (Pos.mul 2) 1%positive p))
+               = ((match (Pos.to_nat p) mod 4 with 0%nat => D1 | 1 => D2 | 2 => D4 | _ => D8 end)%nat Nil,
+                  (Pos.to_nat p / 4)%nat)).
+    { intro p; clear d; rewrite Pos2Nat.inj_iter.
+      fold (Nat.iter (Pos.to_nat p) (Pos.mul 2) 1%positive).
+      set (n := Pos.to_nat p).
+      fold (Nat.iter n t10 1%positive).
+      set (nm4 := (n mod 4)%nat); set (nd4 := (n / 4)%nat).
+      rewrite (Nat.div_mod n 4); [|now simpl].
+      unfold nm4, nd4; clear nm4 nd4.
+      generalize (Nat.mod_upper_bound n 4 ltac:(now simpl)).
+      generalize (n mod 4); generalize (n / 4)%nat.
+      intros d r Hr; clear p n.
+      induction d.
+      { simpl; revert Hr.
+        do 4 (case r; [now simpl|clear r; intro r]).
+        intro H; exfalso.
+        now do 4 (generalize (lt_S_n _ _ H); clear H; intro H). }
+      rewrite Nat.mul_succ_r, <-Nat.add_assoc, (Nat.add_comm 4), Nat.add_assoc.
+      rewrite (Nat.add_comm _ 4).
+      change (4 + _)%nat with (S (S (S (S (4 * d + r))))).
+      rewrite !Unsigned.nat_iter_S.
+      rewrite !Pos.mul_assoc.
+      unfold Pos.to_hex_uint.
+      change (2 * 2 *  2 * 2)%positive with 0x10%positive.
+      set (n := Nat.iter _ _ _).
+      change (Pos.to_little_hex_uint _) with (Unsigned.to_lu (16 * N.pos n)).
+      rewrite Unsigned.to_lhex_tenfold.
+      unfold Hexadecimal.nztail; rewrite rev_rev.
+      rewrite <-(rev_rev (Unsigned.to_lu _)).
+      set (m := _ (rev _)).
+      replace m with (let (r, n) := let (r, n) := m in (rev r, n) in (rev r, n)).
+      2:{ now case m; intros r' n'; rewrite rev_rev. }
+      change (let (r, n) := m in (rev r, n))
+        with (Hexadecimal.nztail (Pos.to_hex_uint n)).
+      now unfold n; rewrite IHd, rev_rev; clear n m. }
+    unfold of_hexadecimal.
+    case d; intros i f; [|intro e]; unfold of_hexadecimal; simpl.
+    - case (Z.of_nat _)%Z; [|intro p..];
+        [now exists (D1 Nil), O; split; [|left]
+        | |now exists (D1 Nil), O; split; [|left]].
+      exists (D1 Nil), (Pos.to_nat p).
+      split; [|now left]; simpl.
+      change (Pos.iter _ _ _) with (Pos.iter (Pos.mul 2) 1%positive (4 * p)).
+      rewrite H.
+      rewrite Pos2Nat.inj_mul, Nat.mul_comm, Nat.div_mul; [|now simpl].
+      now rewrite Nat.mod_mul; [|now simpl].
+    - case (_ - _)%Z; [|intros p..]; [now exists (D1 Nil), O; split; [|left]..|].
+      simpl Qden; rewrite H.
+      eexists; eexists; split; [reflexivity|].
+      case (_ mod _); [now left|intro n].
+      case n; [now right; left|clear n; intro n].
+      case n; [now right; right; left|clear n; intro n].
+      now right; right; right. }
+  generalize (HexadecimalPos.Unsigned.nztail_to_hex_uint (Qden (of_hexadecimal d))).
+  destruct H as (h, (e, (He, Hh))); rewrite He; clear He.
+  assert (Hn1 : forall p, N.pos (Pos.iter (Pos.mul 2) 1%positive p) = 1%N -> False).
+  { intro p.
+    rewrite Pos2Nat.inj_iter.
+    case_eq (Pos.to_nat p); [|now simpl].
+    intro H; exfalso; apply (lt_irrefl O).
+    rewrite <-H at 2; apply Pos2Nat.is_pos. }
+  assert (H16_2 : forall p, (16^p = 2^(4 * p))%positive).
+  { intro p.
+    apply (@f_equal _ _ (fun z => match z with Z.pos p => p | _ => 1%positive end)
+                    (Z.pos _) (Z.pos _)).
+    rewrite !Pos2Z.inj_pow_pos, !Z.pow_pos_fold, Pos2Z.inj_mul.
+    now change 16%Z with (2^4)%Z; rewrite <-Z.pow_mul_r. }
+  assert (HN16_2 : forall n, (16^n = 2^(4 * n))%N).
+  { intro n.
+    apply N2Z.inj; rewrite !N2Z.inj_pow, N2Z.inj_mul.
+    change (Z.of_N 16) with (2^4)%Z.
+    now rewrite <-Z.pow_mul_r; [| |apply N2Z.is_nonneg]. }
+  assert (Hn1' : forall p, N.pos (Pos.iter (Pos.mul 16) 1%positive p) = 1%N -> False).
+  { intro p; fold (16^p)%positive; rewrite H16_2; apply Hn1. }
+  assert (Ht10inj : forall n m, t10 n = t10 m -> n = m).
+  { intros n m H; generalize (f_equal Z.pos H); clear H.
+    change (Z.pos (t10 n)) with (Z.mul 0x10 (Z.pos n)).
+    change (Z.pos (t10 m)) with (Z.mul 0x10 (Z.pos m)).
+    rewrite Z.mul_comm, (Z.mul_comm 0x10).
+    intro H; generalize (f_equal (fun z => Z.div z 0x10) H); clear H.
+    now rewrite !Z.div_mul; [|now simpl..]; intro H; inversion H. }
+  assert (Ht2inj : forall n m, Pos.mul 2 n = Pos.mul 2 m -> n = m).
+  { intros n m H; generalize (f_equal Z.pos H); clear H.
+    change (Z.pos (Pos.mul 2 n)) with (Z.mul 2 (Z.pos n)).
+    change (Z.pos (Pos.mul 2 m)) with (Z.mul 2 (Z.pos m)).
+    rewrite Z.mul_comm, (Z.mul_comm 2).
+    intro H; generalize (f_equal (fun z => Z.div z 2) H); clear H.
+    now rewrite !Z.div_mul; [|now simpl..]; intro H; inversion H. }
+  assert (Hinj : forall n m,
+             Nat.iter n (Pos.mul 2) 1%positive = Nat.iter m (Pos.mul 2) 1%positive
+             -> n = m).
+  { induction n; [now intro m; case m|].
+    intro m; case m; [now simpl|]; clear m; intro m.
+    rewrite !Unsigned.nat_iter_S.
+    intro H; generalize (Ht2inj _ _ H); clear H; intro H.
+    now rewrite (IHn _ H). }
+  change 4%Z with (Z.of_nat 4); rewrite <-Nat2Z.inj_mul.
+  change 1%Z with (Z.of_nat 1); rewrite <-Nat2Z.inj_add.
+  change 2%Z with (Z.of_nat 2); rewrite <-Nat2Z.inj_add.
+  change 3%Z with (Z.of_nat 3); rewrite <-Nat2Z.inj_add.
+  destruct Hh as [Hh|[Hh|[Hh|Hh]]]; rewrite Hh; clear h Hh.
+  - case e; clear e; [|intro e]; simpl; unfold of_hexadecimal, hnorme.
+    + case d; clear d; intros i f; [|intro e].
+      * generalize (nb_digits_pos f).
+        case f;
+          [|now clear f; intro f; intros H1 H2; exfalso; revert H1 H2;
+            case nb_digits;
+            [intros H _; apply (lt_irrefl O), H|intros n _; apply Hn1]..].
+        now intros _ _; simpl; rewrite to_of.
+      * rewrite <-DecimalZ.to_of, DecimalZ.of_to.
+        set (emf := (_ - _)%Z).
+        case_eq emf; [|intro pemf..].
+        ++ now simpl; rewrite to_of.
+        ++ intros Hemf _; simpl.
+           apply f_equal, f_equal2; [|reflexivity].
+           rewrite !Pos2Nat.inj_iter.
+           fold (Nat.iter (Pos.to_nat pemf) (Z.mul 2) (Z.of_hex_int (app_int i f))).
+           fold (Nat.iter (Pos.to_nat pemf) double (norm (app_int i f))).
+           induction Pos.to_nat; [now simpl; rewrite HexadecimalZ.to_of|].
+           now rewrite !Unsigned.nat_iter_S, <-IHn, double_to_hex_int.
+        ++ simpl Qden; intros _ H; exfalso; revert H; apply Hn1.
+    + case d; clear d; intros i f; [|intro e'].
+      * simpl; case_eq (nb_digits f); [|intros nf' Hnf'];
+          [now simpl; intros _ H; exfalso; symmetry in H; revert H; apply Hn1'|].
+        unfold Z.of_nat, Z.opp, Qnum, Qden.
+        rewrite H16_2.
+        fold (Pos.mul 2); fold (2^(Pos.of_succ_nat nf')~0~0)%positive.
+        intro H; injection H; clear H.
+        unfold Pos.pow; rewrite !Pos2Nat.inj_iter.
+        intro H; generalize (Hinj _ _ H); clear H; intro H.
+        generalize (Pos2Nat.inj _ _ H); clear H; intro H; injection H.
+        clear H; intro H; generalize (SuccNat2Pos.inj _ _ H); clear H.
+        intros <-.
+        rewrite to_of.
+        rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
+        do 4 apply f_equal.
+        apply Pos2Nat.inj.
+        rewrite SuccNat2Pos.id_succ.
+        change (_~0)%positive with (4 * Pos.of_succ_nat nf')%positive.
+        now rewrite Pos2Nat.inj_mul, SuccNat2Pos.id_succ.
+      * set (nemf := (_ - _)%Z); intro H.
+        assert (H' : exists pnemf, nemf = Z.neg pnemf); [|revert H].
+        { revert H; case nemf; [|intro pnemf..]; [..|now intros _; exists pnemf];
+            simpl Qden; intro H; exfalso; symmetry in H; revert H; apply Hn1'. }
+        destruct H' as (pnemf,Hpnemf); rewrite Hpnemf.
+        unfold Qnum, Qden.
+        rewrite H16_2.
+        intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter.
+        intro H; generalize (Hinj _ _ H); clear H; intro H.
+        generalize (Pos2Nat.inj _ _ H); clear H.
+        intro H; revert Hpnemf; rewrite H; clear pnemf H; intro Hnemf.
+        rewrite to_of.
+        rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
+        do 4 apply f_equal.
+        apply Pos2Nat.inj.
+        rewrite SuccNat2Pos.id_succ.
+        change (_~0)%positive with (4 * Pos.of_succ_nat e)%positive.
+        now rewrite Pos2Nat.inj_mul, SuccNat2Pos.id_succ.
+  - simpl Pos.of_hex_uint.
+    rewrite HN16_2.
+    rewrite <-N.pow_succ_r; [|now apply N.le_0_l].
+    rewrite <-N.succ_pos_spec.
+    case d; clear d; intros i f; [|intro e']; unfold of_hexadecimal, hnorme.
+    + set (em4f := (_ - _)%Z).
+      case_eq em4f; [|intros pem4f..]; intro Hpem4f;
+        [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|].
+      unfold Qnum, Qden.
+      intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter.
+      intro H; generalize (Hinj _ _ H); clear H; intro H.
+      generalize (Pos2Nat.inj _ _ H); clear H; intros ->.
+      rewrite to_of.
+      rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
+      do 4 apply f_equal.
+      apply Pos2Nat.inj.
+      rewrite SuccNat2Pos.id_succ.
+      case e; [now simpl|intro e'']; simpl.
+      unfold Pos.to_nat; simpl.
+      now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm.
+    + set (em4f := (_ - _)%Z).
+      case_eq em4f; [|intros pem4f..]; intro Hpem4f;
+        [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|].
+      unfold Qnum, Qden.
+      intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter.
+      intro H; generalize (Hinj _ _ H); clear H; intro H.
+      generalize (Pos2Nat.inj _ _ H); clear H; intros ->.
+      rewrite to_of.
+      rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
+      do 4 apply f_equal.
+      apply Pos2Nat.inj.
+      rewrite SuccNat2Pos.id_succ.
+      case e; [now simpl|intro e'']; simpl.
+      unfold Pos.to_nat; simpl.
+      now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm.
+  - simpl Pos.of_hex_uint.
+    rewrite HN16_2.
+    change 4%N with (2 * 2)%N at 1; rewrite <-!N.mul_assoc.
+    do 2 (rewrite <-N.pow_succ_r; [|now apply N.le_0_l]).
+    rewrite <-N.succ_pos_spec.
+    case d; clear d; intros i f; [|intro e']; unfold of_hexadecimal, hnorme.
+    + set (em4f := (_ - _)%Z).
+      case_eq em4f; [|intros pem4f..]; intro Hpem4f;
+        [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|].
+      unfold Qnum, Qden.
+      intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter.
+      intro H; generalize (Hinj _ _ H); clear H; intro H.
+      generalize (Pos2Nat.inj _ _ H); clear H; intros ->.
+      rewrite to_of.
+      rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
+      do 4 apply f_equal.
+      apply Pos2Nat.inj.
+      rewrite <-SuccNat2Pos.inj_succ.
+      rewrite SuccNat2Pos.id_succ.
+      case e; [now simpl|intro e'']; simpl.
+      unfold Pos.to_nat; simpl.
+      now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm.
+    + set (em4f := (_ - _)%Z).
+      case_eq em4f; [|intros pem4f..]; intro Hpem4f;
+        [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|].
+      unfold Qnum, Qden.
+      intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter.
+      intro H; generalize (Hinj _ _ H); clear H; intro H.
+      generalize (Pos2Nat.inj _ _ H); clear H; intros ->.
+      rewrite to_of.
+      rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
+      do 4 apply f_equal.
+      apply Pos2Nat.inj.
+      rewrite <-SuccNat2Pos.inj_succ.
+      rewrite SuccNat2Pos.id_succ.
+      case e; [now simpl|intro e'']; simpl.
+      unfold Pos.to_nat; simpl.
+      now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm.
+  - simpl Pos.of_hex_uint.
+    rewrite HN16_2.
+    change 8%N with (2 * 2 * 2)%N; rewrite <-!N.mul_assoc.
+    do 3 (rewrite <-N.pow_succ_r; [|now apply N.le_0_l]).
+    rewrite <-N.succ_pos_spec.
+    case d; clear d; intros i f; [|intro e']; unfold of_hexadecimal, hnorme.
+    + set (em4f := (_ - _)%Z).
+      case_eq em4f; [|intros pem4f..]; intro Hpem4f;
+        [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|].
+      unfold Qnum, Qden.
+      intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter.
+      intro H; generalize (Hinj _ _ H); clear H; intro H.
+      generalize (Pos2Nat.inj _ _ H); clear H; intros ->.
+      rewrite to_of.
+      rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
+      do 4 apply f_equal.
+      apply Pos2Nat.inj.
+      rewrite <-!SuccNat2Pos.inj_succ.
+      rewrite SuccNat2Pos.id_succ.
+      case e; [now simpl|intro e'']; simpl.
+      unfold Pos.to_nat; simpl.
+      now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm.
+    + set (em4f := (_ - _)%Z).
+      case_eq em4f; [|intros pem4f..]; intro Hpem4f;
+        [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|].
+      unfold Qnum, Qden.
+      intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter.
+      intro H; generalize (Hinj _ _ H); clear H; intro H.
+      generalize (Pos2Nat.inj _ _ H); clear H; intros ->.
+      rewrite to_of.
+      rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
+      do 4 apply f_equal.
+      apply Pos2Nat.inj.
+      rewrite <-!SuccNat2Pos.inj_succ.
+      rewrite SuccNat2Pos.id_succ.
+      case e; [now simpl|intro e'']; simpl.
+      unfold Pos.to_nat; simpl.
+      now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm.
+Qed.
+
+(** Some consequences *)
+
+Lemma to_hexadecimal_inj q q' :
+  to_hexadecimal q <> None -> to_hexadecimal q = to_hexadecimal q' -> q = q'.
+Proof.
+  intros Hnone EQ.
+  generalize (of_to q) (of_to q').
+  rewrite <-EQ.
+  revert Hnone; case to_hexadecimal; [|now simpl].
+  now intros d _ H1 H2; rewrite <-(H1 d eq_refl), <-(H2 d eq_refl).
+Qed.
+
+Lemma to_hexadecimal_surj d : exists q, to_hexadecimal q = Some (hnorme d).
+Proof.
+  exists (of_hexadecimal d). apply to_of.
+Qed.
+
+Lemma of_hexadecimal_hnorme d : of_hexadecimal (hnorme d) = of_hexadecimal d.
+Proof.
+  unfold of_hexadecimal, hnorme.
+  destruct d.
+  - simpl Z.of_int; unfold Z.of_uint, Z.of_N, Pos.of_uint.
+    rewrite Z.sub_0_l.
+    set (n4f := (- _)%Z).
+    case_eq n4f; [|intro pn4f..]; intro Hn4f.
+    + apply f_equal2; [|reflexivity].
+      rewrite app_int_nil_r.
+      now rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to.
+    + apply f_equal2; [|reflexivity].
+      rewrite app_int_nil_r.
+      generalize (app_int i f); intro i'.
+      rewrite !Pos2Nat.inj_iter.
+      generalize (Pos.to_nat pn4f); intro n.
+      fold (Nat.iter n double (norm i')).
+      fold (Nat.iter n (Z.mul 2) (Z.of_hex_int i')).
+      induction n; [now simpl; rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to|].
+      now rewrite !Unsigned.nat_iter_S, <-IHn, of_hex_int_double.
+    + unfold nb_digits, Z.of_nat.
+      rewrite Z.mul_0_r, Z.sub_0_r.
+      rewrite <-DecimalZ.to_of, !DecimalZ.of_to.
+      rewrite app_int_nil_r.
+      now rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to.
+  - set (nem4f := (_ - _)%Z).
+    case_eq nem4f; [|intro pnem4f..]; intro Hnem4f.
+    + apply f_equal2; [|reflexivity].
+      rewrite app_int_nil_r.
+      now rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to.
+    + apply f_equal2; [|reflexivity].
+      rewrite app_int_nil_r.
+      generalize (app_int i f); intro i'.
+      rewrite !Pos2Nat.inj_iter.
+      generalize (Pos.to_nat pnem4f); intro n.
+      fold (Nat.iter n double (norm i')).
+      fold (Nat.iter n (Z.mul 2) (Z.of_hex_int i')).
+      induction n; [now simpl; rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to|].
+      now rewrite !Unsigned.nat_iter_S, <-IHn, of_hex_int_double.
+    + unfold nb_digits, Z.of_nat.
+      rewrite Z.mul_0_r, Z.sub_0_r.
+      rewrite <-DecimalZ.to_of, !DecimalZ.of_to.
+      rewrite app_int_nil_r.
+      now rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to.
+Qed.
+
+Lemma of_inj d d' :
+  of_hexadecimal d = of_hexadecimal d' -> hnorme d = hnorme d'.
+Proof.
+  intros.
+  cut (Some (hnorme d) = Some (hnorme d')); [now intro H'; injection H'|].
+  rewrite <- !to_of. now f_equal.
+Qed.
+
+Lemma of_iff d d' :
+  of_hexadecimal d = of_hexadecimal d' <-> hnorme d = hnorme d'.
+Proof.
+  split. apply of_inj. intros E. rewrite <- of_hexadecimal_hnorme, E.
+  apply of_hexadecimal_hnorme.
+Qed.
diff --git a/theories/Numbers/HexadecimalZ.v b/theories/Numbers/HexadecimalZ.v
new file mode 100644
index 0000000000..c5ed0b5b28
--- /dev/null
+++ b/theories/Numbers/HexadecimalZ.v
@@ -0,0 +1,142 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** * HexadecimalZ
+
+    Proofs that conversions between hexadecimal numbers and [Z]
+    are bijections. *)
+
+Require Import Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN ZArith.
+
+Lemma of_to (z:Z) : Z.of_hex_int (Z.to_hex_int z) = z.
+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.
+
+Lemma to_of (d:int) : Z.to_hex_int (Z.of_hex_int d) = norm d.
+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.
+
+(** Some consequences *)
+
+Lemma to_int_inj n n' : Z.to_hex_int n = Z.to_hex_int n' -> n = n'.
+Proof.
+  intro EQ.
+  now rewrite <- (of_to n), <- (of_to n'), EQ.
+Qed.
+
+Lemma to_int_surj d : exists n, Z.to_hex_int n = norm d.
+Proof.
+  exists (Z.of_hex_int d). apply to_of.
+Qed.
+
+Lemma of_int_norm d : Z.of_hex_int (norm d) = Z.of_hex_int d.
+Proof.
+  unfold Z.of_hex_int, Z.of_hex_uint.
+  destruct d.
+  - simpl. now rewrite HexadecimalPos.Unsigned.of_uint_norm.
+  - simpl. destruct (nzhead d) eqn:H;
+    [ induction d; simpl; auto; discriminate |
+      destruct (nzhead_nonzero _ _ H) | .. ];
+    f_equal; f_equal; apply HexadecimalPos.Unsigned.of_iff;
+      unfold unorm; now rewrite H.
+Qed.
+
+Lemma of_inj d d' :
+  Z.of_hex_int d = Z.of_hex_int d' -> norm d = norm d'.
+Proof.
+  intros. rewrite <- !to_of. now f_equal.
+Qed.
+
+Lemma of_iff d d' : Z.of_hex_int d = Z.of_hex_int d' <-> norm d = norm d'.
+Proof.
+  split. apply of_inj. intros E. rewrite <- of_int_norm, E.
+  apply of_int_norm.
+Qed.
+
+(** Various lemmas *)
+
+Lemma of_hex_uint_iter_D0 d n :
+  Z.of_hex_uint (app d (Nat.iter n D0 Nil))
+  = Nat.iter n (Z.mul 0x10) (Z.of_hex_uint d).
+Proof.
+  unfold Z.of_hex_uint.
+  unfold app; rewrite <-rev_revapp.
+  rewrite Unsigned.of_lu_rev, Unsigned.of_lu_revapp.
+  rewrite <-!Unsigned.of_lu_rev, !rev_rev.
+  assert (H' : Pos.of_hex_uint (Nat.iter n D0 Nil) = 0%N).
+  { now induction n; [|rewrite Unsigned.nat_iter_S]. }
+  rewrite H', N.add_0_l; clear H'.
+  induction n; [now simpl; rewrite N.mul_1_r|].
+  rewrite !Unsigned.nat_iter_S, <-IHn.
+  simpl Unsigned.usize; rewrite N.pow_succ_r'.
+  rewrite !N2Z.inj_mul; simpl Z.of_N; ring.
+Qed.
+
+Lemma of_hex_int_iter_D0 d n :
+  Z.of_hex_int (app_int d (Nat.iter n D0 Nil))
+  = Nat.iter n (Z.mul 0x10) (Z.of_hex_int d).
+Proof.
+  case d; clear d; intro d; simpl.
+  - now rewrite of_hex_uint_iter_D0.
+  - rewrite of_hex_uint_iter_D0; induction n; [now simpl|].
+    rewrite !Unsigned.nat_iter_S, <-IHn; ring.
+Qed.
+
+Definition double d :=
+  match d with
+  | Pos u => Pos (Unsigned.double u)
+  | Neg u => Neg (Unsigned.double u)
+  end.
+
+Lemma double_norm d : double (norm d) = norm (double d).
+Proof.
+  destruct d.
+  - now simpl; rewrite Unsigned.double_unorm.
+  - simpl; rewrite <-Unsigned.double_nzhead.
+    case (uint_eq_dec (nzhead d) Nil); intro Hnzd.
+    + now rewrite Hnzd.
+    + assert (H : Unsigned.double (nzhead d) <> Nil).
+      { unfold Unsigned.double.
+        intro H; apply Hnzd, rev_nil_inv.
+        now generalize (rev_nil_inv _ H); case rev. }
+      revert H.
+      set (r := Unsigned.double _).
+      set (m := match r with Nil => Pos zero | _ => _ end).
+      intro H.
+      assert (H' : m = Neg r).
+      { now unfold m; clear m; revert H; case r. }
+      rewrite H'; unfold r; clear m r H H'.
+      now revert Hnzd; case nzhead.
+Qed.
+
+Lemma of_hex_int_double d :
+  Z.of_hex_int (double d) = Z.double (Z.of_hex_int d).
+Proof.
+  now destruct d; simpl; unfold Z.of_hex_uint;
+    rewrite Unsigned.of_hex_uint_double; case Pos.of_hex_uint.
+Qed.
+
+Lemma double_to_hex_int n :
+  double (Z.to_hex_int n) = Z.to_hex_int (Z.double n).
+Proof. now rewrite <-(of_to n), <-of_hex_int_double, !to_of, double_norm. Qed.