Merge PR #12218: Numeral notations for non inductive types

Reviewed-by: herbelin
Reviewed-by: JasonGross
Reviewed-by: jfehrle
Ack-by: Zimmi48

13 files changed, 2405 insertions, 1289 deletions

diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v
index 7c846571a7..c203c178f5 100644
--- a/theories/Numbers/AltBinNotations.v
+++ b/theories/Numbers/AltBinNotations.v
@@ -17,7 +17,7 @@
     the [Decimal.int] representation. When working with numbers with
     thousands of digits and more, conversion from/to [Decimal.int] can
     become significantly slow. If that becomes a problem for your
-    development, this file provides some alternative [Numeral
+    development, this file provides some alternative [Number
     Notation] commands that use [Z] as bridge type. To enable these
     commands, just be sure to [Require] this file after other files
     defining numeral notations.
diff --git a/theories/Numbers/DecimalFacts.v b/theories/Numbers/DecimalFacts.v
index dd361562ba..87a9f704cd 100644
--- a/theories/Numbers/DecimalFacts.v
+++ b/theories/Numbers/DecimalFacts.v
@@ -10,175 +10,425 @@
 
 (** * DecimalFacts : some facts about Decimal numbers *)
 
-Require Import Decimal Arith.
+Require Import Decimal Arith ZArith.
+
+Variant digits := d0 | d1 | d2 | d3 | d4 | d5 | d6 | d7 | d8 | d9.
+
+Fixpoint to_list (u : uint) : list digits :=
+  match u with
+  | Nil => nil
+  | D0 u => cons d0 (to_list u)
+  | D1 u => cons d1 (to_list u)
+  | D2 u => cons d2 (to_list u)
+  | D3 u => cons d3 (to_list u)
+  | D4 u => cons d4 (to_list u)
+  | D5 u => cons d5 (to_list u)
+  | D6 u => cons d6 (to_list u)
+  | D7 u => cons d7 (to_list u)
+  | D8 u => cons d8 (to_list u)
+  | D9 u => cons d9 (to_list u)
+  end.
 
-Lemma uint_dec (d d' : uint) : { d = d' } + { d <> d' }.
-Proof.
-  decide equality.
-Defined.
+Fixpoint of_list (l : list digits) : uint :=
+  match l with
+  | nil => Nil
+  | cons d0 l => D0 (of_list l)
+  | cons d1 l => D1 (of_list l)
+  | cons d2 l => D2 (of_list l)
+  | cons d3 l => D3 (of_list l)
+  | cons d4 l => D4 (of_list l)
+  | cons d5 l => D5 (of_list l)
+  | cons d6 l => D6 (of_list l)
+  | cons d7 l => D7 (of_list l)
+  | cons d8 l => D8 (of_list l)
+  | cons d9 l => D9 (of_list l)
+  end.
 
-Lemma rev_revapp d d' :
-  rev (revapp d d') = revapp d' d.
+Lemma of_list_to_list u : of_list (to_list u) = u.
+Proof. now induction u; [|simpl; rewrite IHu..]. Qed.
+
+Lemma to_list_of_list l : to_list (of_list l) = l.
+Proof. now induction l as [|h t IHl]; [|case h; simpl; rewrite IHl]. Qed.
+
+Lemma to_list_inj u u' : to_list u = to_list u' -> u = u'.
 Proof.
-  revert d'. induction d; simpl; intros; now rewrite ?IHd.
+  now intro H; rewrite <-(of_list_to_list u), <-(of_list_to_list u'), H.
 Qed.
 
-Lemma rev_rev d : rev (rev d) = d.
+Lemma of_list_inj u u' : of_list u = of_list u' -> u = u'.
 Proof.
-  apply rev_revapp.
+  now intro H; rewrite <-(to_list_of_list u), <-(to_list_of_list u'), H.
 Qed.
 
-Lemma revapp_rev_nil d : revapp (rev d) Nil = d.
-Proof. now fold (rev (rev d)); rewrite rev_rev. Qed.
+Lemma nb_digits_spec u : nb_digits u = length (to_list u).
+Proof. now induction u; [|simpl; rewrite IHu..]. Qed.
 
-Lemma app_nil_r d : app d Nil = d.
-Proof. now unfold app; rewrite revapp_rev_nil. Qed.
+Fixpoint lnzhead l :=
+  match l with
+  | nil => nil
+  | cons d l' =>
+    match d with
+    | d0 => lnzhead l'
+    | _ => l
+    end
+  end.
 
-Lemma app_int_nil_r d : app_int d Nil = d.
-Proof. now case d; intro d'; simpl; rewrite app_nil_r. Qed.
+Lemma nzhead_spec u : to_list (nzhead u) = lnzhead (to_list u).
+Proof. now induction u; [|simpl; rewrite IHu|..]. Qed.
+
+Definition lzero := cons d0 nil.
+
+Definition lunorm l :=
+  match lnzhead l with
+  | nil => lzero
+  | d => d
+  end.
+
+Lemma unorm_spec u : to_list (unorm u) = lunorm (to_list u).
+Proof. now unfold unorm, lunorm; rewrite <-nzhead_spec; case (nzhead u). Qed.
 
-Lemma revapp_revapp_1 d d' d'' :
-  nb_digits d <= 1 ->
-  revapp (revapp d d') d'' = revapp d' (revapp d d'').
+Lemma revapp_spec d d' :
+  to_list (revapp d d') = List.rev_append (to_list d) (to_list d').
+Proof. now revert d'; induction d; intro d'; [|simpl; rewrite IHd..]. Qed.
+
+Lemma rev_spec d : to_list (rev d) = List.rev (to_list d).
+Proof. now unfold rev; rewrite revapp_spec, List.rev_alt; simpl. Qed.
+
+Lemma app_spec d d' :
+  to_list (app d d') = Datatypes.app (to_list d) (to_list 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))]..]..].
+  unfold app.
+  now rewrite revapp_spec, List.rev_append_rev, rev_spec, List.rev_involutive.
 Qed.
 
-Lemma nb_digits_pos d : d <> Nil -> 0 < nb_digits d.
-Proof. now case d; [|intros d' _; apply Nat.lt_0_succ..]. Qed.
+Definition lnztail l :=
+  let fix aux l_rev :=
+    match l_rev with
+    | cons d0 l_rev => let (r, n) := aux l_rev in pair r (S n)
+    | _ => pair l_rev O
+    end in
+  let (r, n) := aux (List.rev l) in pair (List.rev r) n.
 
-Lemma nb_digits_revapp d d' :
-  nb_digits (revapp d d') = nb_digits d + nb_digits d'.
+Lemma nztail_spec d :
+  let (r, n) := nztail d in
+  let (r', n') := lnztail (to_list d) in
+  to_list r = r' /\ n = n'.
 Proof.
-  now revert d'; induction d; [|intro d'; simpl; rewrite IHd; simpl..].
+  unfold nztail, lnztail.
+  set (f := fix aux d_rev := match d_rev with
+            | D0 d_rev => let (r, n) := aux d_rev in (r, S n)
+            | _ => (d_rev, 0) end).
+  set (f' := fix aux (l_rev : list digits) : list digits * nat :=
+             match l_rev with
+             | cons d0 l_rev => let (r, n) := aux l_rev in (r, S n)
+             | _ => (l_rev, 0)
+             end).
+  rewrite <-(of_list_to_list (rev d)), rev_spec.
+  induction (List.rev _) as [|h t IHl]; [now simpl|].
+  case h; simpl; [|now rewrite rev_spec; simpl; rewrite to_list_of_list..].
+  now revert IHl; case f; intros r n; case f'; intros r' n' [-> ->].
 Qed.
 
-Lemma nb_digits_rev u : nb_digits (rev u) = nb_digits u.
-Proof. now unfold rev; rewrite nb_digits_revapp. Qed.
+Lemma del_head_spec_0 d : del_head 0 d = d.
+Proof. now simpl. Qed.
 
-Lemma nb_digits_nzhead u : nb_digits (nzhead u) <= nb_digits u.
-Proof. now induction u; [|apply le_S|..]. Qed.
+Lemma del_head_spec_small n d :
+  n <= length (to_list d) -> to_list (del_head n d) = List.skipn n (to_list d).
+Proof.
+  revert d; induction n as [|n IHn]; intro d; [now simpl|].
+  now case d; [|intros d' H; apply IHn, le_S_n..].
+Qed.
 
-Lemma del_head_nb_digits (u:uint) : del_head (nb_digits u) u = Nil.
-Proof. now induction u. Qed.
+Lemma del_head_spec_large n d : length (to_list d) < n -> del_head n d = zero.
+Proof.
+  revert d; induction n; intro d; [now case d|].
+  now case d; [|intro d'; simpl; intro H; rewrite (IHn _ (lt_S_n _ _ H))..].
+Qed.
 
-Lemma nb_digits_del_head n u :
-  n <= nb_digits u -> nb_digits (del_head n u) = nb_digits u - n.
+Lemma nb_digits_0 d : nb_digits d = 0 -> d = Nil.
 Proof.
-  revert u; induction n; intros u; [now rewrite Nat.sub_0_r|].
-  now case u; clear u; intro u; [|intro Hn; apply IHn, le_S_n..].
+  rewrite nb_digits_spec, <-(of_list_to_list d).
+  now case (to_list d) as [|h t]; [|rewrite to_list_of_list].
 Qed.
 
+Lemma nb_digits_n0 d : nb_digits d <> 0 -> d <> Nil.
+Proof. now case d; [|intros u _..]. 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
-    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 =>
-      nth n d
-    end
-  end.
+Lemma length_lnzhead l : length (lnzhead l) <= length l.
+Proof. now induction l as [|h t IHl]; [|case h; [apply le_S|..]]. Qed.
+
+Lemma nb_digits_nzhead u : nb_digits (nzhead u) <= nb_digits u.
+Proof. now induction u; [|apply le_S|..]. Qed.
+
+Lemma unorm_nzhead u : nzhead u <> Nil -> unorm u = nzhead u.
+Proof. now unfold unorm; case nzhead. Qed.
 
-Lemma nb_digits_nth n u : nb_digits (nth n u) <= 1.
+Lemma nb_digits_unorm u : u <> Nil -> nb_digits (unorm u) <= nb_digits u.
 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..].
+  intro Hu; case (uint_eq_dec (nzhead u) Nil).
+  { unfold unorm; intros ->; simpl.
+    now revert Hu; case u; [|intros u' _; apply le_n_S, Nat.le_0_l..]. }
+  intro H; rewrite (unorm_nzhead _ H); apply nb_digits_nzhead.
 Qed.
 
-Lemma del_head_nth n u :
-  n < nb_digits u ->
-  del_head n u = revapp (nth n u) (del_head (S n) u).
-Proof.
-  revert u; induction n; intro u; [now case u|].
-  now case u; [|intro u'; intro H; apply IHn, le_S_n..].
-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.
-
-Lemma app_del_tail_head (u:uint) n :
-  n <= nb_digits u ->
-  app (del_tail n u) (del_head (nb_digits u - n) u) = u.
-Proof.
-  unfold app, del_tail; rewrite rev_rev.
-  induction n.
-  - intros _; rewrite Nat.sub_0_r, del_head_nb_digits; simpl.
-    now rewrite revapp_rev_nil.
-  - intro Hn.
-    rewrite (del_head_nth (_ - _));
-      [|now apply Nat.sub_lt; [|apply Nat.lt_0_succ]].
-    rewrite Nat.sub_succ_r, <-Nat.sub_1_r.
-    rewrite <-(nth_revapp_l _ _ Nil Hn); fold (rev u).
-    rewrite <-revapp_revapp_1; [|now apply nb_digits_nth].
-    rewrite <-(del_head_nth _ _); [|now rewrite nb_digits_rev].
-    rewrite Nat.sub_1_r, Nat.succ_pred_pos; [|now apply Nat.lt_add_lt_sub_r].
-    apply (IHn (le_Sn_le _ _ Hn)).
+Lemma nb_digits_rev d : nb_digits (rev d) = nb_digits d.
+Proof. now rewrite !nb_digits_spec, rev_spec, List.rev_length. Qed.
+
+Lemma nb_digits_del_head_sub d n :
+  n <= nb_digits d ->
+  nb_digits (del_head (nb_digits d - n) d) = n.
+Proof.
+  rewrite !nb_digits_spec; intro Hn.
+  rewrite del_head_spec_small; [|now apply Nat.le_sub_l].
+  rewrite List.skipn_length, <-(Nat2Z.id (_ - _)).
+  rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l].
+  rewrite (Nat2Z.inj_sub _ _ Hn).
+  rewrite Z.sub_sub_distr, Z.sub_diag; apply Nat2Z.id.
+Qed.
+
+Lemma unorm_D0 u : unorm (D0 u) = unorm u.
+Proof. reflexivity. Qed.
+
+Lemma app_nil_l d : app Nil d = d.
+Proof. now simpl. Qed.
+
+Lemma app_nil_r d : app d Nil = d.
+Proof. now apply to_list_inj; rewrite app_spec, List.app_nil_r. Qed.
+
+Lemma abs_app_int d d' : abs (app_int d d') = app (abs d) d'.
+Proof. now case d. Qed.
+
+Lemma abs_norm d : abs (norm d) = unorm (abs d).
+Proof. now case d as [u|u]; [|simpl; unfold unorm; case nzhead]. Qed.
+
+Lemma iter_D0_nzhead d :
+  Nat.iter (nb_digits d - nb_digits (nzhead d)) D0 (nzhead d) = d.
+Proof.
+  induction d; [now simpl| |now rewrite Nat.sub_diag..].
+  simpl nzhead; simpl nb_digits.
+  rewrite (Nat.sub_succ_l _ _ (nb_digits_nzhead _)).
+  now rewrite <-IHd at 4.
+Qed.
+
+Lemma iter_D0_unorm d :
+  d <> Nil ->
+  Nat.iter (nb_digits d - nb_digits (unorm d)) D0 (unorm d) = d.
+Proof.
+  case (uint_eq_dec (nzhead d) Nil); intro Hn.
+  { unfold unorm; rewrite Hn; simpl; intro H.
+    revert H Hn; induction d; [now simpl|intros _|now intros _..].
+    case (uint_eq_dec d Nil); simpl; intros H Hn; [now rewrite H|].
+    rewrite Nat.sub_0_r, (le_plus_minus 1 (nb_digits d)).
+    { now simpl; rewrite IHd. }
+    revert H; case d; [now simpl|intros u _; apply le_n_S, Nat.le_0_l..]. }
+  intros _; rewrite (unorm_nzhead _ Hn); apply iter_D0_nzhead.
+Qed.
+
+Lemma nzhead_app_l d d' :
+  nb_digits d' < nb_digits (nzhead (app d d')) ->
+  nzhead (app d d') = app (nzhead d) d'.
+Proof.
+  intro Hl; apply to_list_inj; revert Hl.
+  rewrite !nb_digits_spec, app_spec, !nzhead_spec, app_spec.
+  induction (to_list d) as [|h t IHl].
+  { now simpl; intro H; exfalso; revert H; apply le_not_lt, length_lnzhead. }
+  rewrite <-List.app_comm_cons.
+  now case h; [simpl; intro Hl; apply IHl|..].
+Qed.
+
+Lemma nzhead_app_r d d' :
+  nb_digits (nzhead (app d d')) <= nb_digits d' ->
+  nzhead (app d d') = nzhead d'.
+Proof.
+  intro Hl; apply to_list_inj; revert Hl.
+  rewrite !nb_digits_spec, !nzhead_spec, app_spec.
+  induction (to_list d) as [|h t IHl]; [now simpl|].
+  rewrite <-List.app_comm_cons.
+  now case h; [| simpl; rewrite List.app_length; intro Hl; exfalso; revert Hl;
+    apply le_not_lt, le_plus_r..].
+Qed.
+
+Lemma nzhead_app_nil_r d d' : nzhead (app d d') = Nil -> nzhead d' = Nil.
+Proof.
+now intro H; generalize H; rewrite nzhead_app_r; [|rewrite H; apply Nat.le_0_l].
+Qed.
+
+Lemma nzhead_app_nil d d' :
+  nb_digits (nzhead (app d d')) <= nb_digits d' -> nzhead d = Nil.
+Proof.
+  intro H; apply to_list_inj; revert H.
+  rewrite !nb_digits_spec, !nzhead_spec, app_spec.
+  induction (to_list d) as [|h t IHl]; [now simpl|].
+  now case h; [now simpl|..];
+    simpl;intro H; exfalso; revert H; apply le_not_lt;
+    rewrite List.app_length; apply le_plus_r.
+Qed.
+
+Lemma nzhead_app_nil_l d d' : nzhead (app d d') = Nil -> nzhead d = Nil.
+Proof.
+  intro H; apply to_list_inj; generalize (f_equal to_list H); clear H.
+  rewrite !nzhead_spec, app_spec.
+  induction (to_list d) as [|h t IHl]; [now simpl|].
+  now rewrite <-List.app_comm_cons; case h.
+Qed.
+
+Lemma unorm_app_zero d d' :
+  nb_digits (unorm (app d d')) <= nb_digits d' -> unorm d = zero.
+Proof.
+  unfold unorm.
+  case (uint_eq_dec (nzhead (app d d')) Nil).
+  { now intro Hn; rewrite Hn, (nzhead_app_nil_l _ _ Hn). }
+  intro H; fold (unorm (app d d')); rewrite (unorm_nzhead _ H); intro H'.
+  case (uint_eq_dec (nzhead d) Nil); [now intros->|].
+  intro H''; fold (unorm d); rewrite (unorm_nzhead _ H'').
+  exfalso; apply H''; revert H'; apply nzhead_app_nil.
+Qed.
+
+Lemma app_int_nil_r d : app_int d Nil = d.
+Proof.
+  now case d; intro d'; simpl;
+    rewrite <-(of_list_to_list (app _ _)), app_spec;
+    rewrite List.app_nil_r, of_list_to_list.
+Qed.
+
+Lemma unorm_app_l d d' :
+  nb_digits d' < nb_digits (unorm (app d d')) ->
+  unorm (app d d') = app (unorm d) d'.
+Proof.
+  case (uint_eq_dec d' Nil); [now intros->; rewrite !app_nil_r|intro Hd'].
+  case (uint_eq_dec (nzhead (app d d')) Nil).
+  { unfold unorm; intros->; simpl; intro H; exfalso; revert H; apply le_not_lt.
+    now revert Hd'; case d'; [|intros d'' _; apply le_n_S, Peano.le_0_n..]. }
+  intro Ha; rewrite (unorm_nzhead _ Ha).
+  intro Hn; generalize Hn; rewrite (nzhead_app_l _ _ Hn).
+  rewrite !nb_digits_spec, app_spec, List.app_length.
+  case (uint_eq_dec (nzhead d) Nil).
+  { intros->; simpl; intro H; exfalso; revert H; apply Nat.lt_irrefl. }
+  now intro H; rewrite (unorm_nzhead _ H).
+Qed.
+
+Lemma unorm_app_r d d' :
+  nb_digits (unorm (app d d')) <= nb_digits d' ->
+  unorm (app d d') = unorm d'.
+Proof.
+  case (uint_eq_dec (nzhead (app d d')) Nil).
+  { now unfold unorm; intro H; rewrite H, (nzhead_app_nil_r _ _ H). }
+  intro Ha; rewrite (unorm_nzhead _ Ha).
+  case (uint_eq_dec (nzhead d') Nil).
+  { now intros H H'; exfalso; apply Ha; rewrite nzhead_app_r. }
+  intro Hd'; rewrite (unorm_nzhead _ Hd'); apply nzhead_app_r.
+Qed.
+
+Lemma norm_app_int d d' :
+  nb_digits d' < nb_digits (unorm (app (abs d) d')) ->
+  norm (app_int d d') = app_int (norm d) d'.
+Proof.
+  case (uint_eq_dec d' Nil); [now intros->; rewrite !app_int_nil_r|intro Hd'].
+  case d as [d|d]; [now simpl; intro H; apply f_equal, unorm_app_l|].
+  simpl; unfold unorm.
+  case (uint_eq_dec (nzhead (app d d')) Nil).
+  { intros->; simpl; intro H; exfalso; revert H; apply le_not_lt.
+    now revert Hd'; case d'; [|intros d'' _; apply le_n_S, Peano.le_0_n..]. }
+  set (m := match nzhead _ with Nil => _ | _ => _ end).
+  intro Ha.
+  replace m with (nzhead (app d d')).
+  2:{ now unfold m; revert Ha; case nzhead. }
+  intro Hn; generalize Hn; rewrite (nzhead_app_l _ _ Hn).
+  case (uint_eq_dec (app (nzhead d) d') Nil).
+  { intros->; simpl; intro H; exfalso; revert H; apply le_not_lt, Nat.le_0_l. }
+  clear m; set (m := match app _ _ with Nil => _ | _ => _ end).
+  intro Ha'.
+  replace m with (Neg (app (nzhead d) d')); [|now unfold m; revert Ha'; case app].
+  case (uint_eq_dec (nzhead d) Nil).
+  { intros->; simpl; intro H; exfalso; revert H; apply Nat.lt_irrefl. }
+  clear m; set (m := match nzhead _ with Nil => _ | _ => _ end).
+  intro Hd.
+  now replace m with (Neg (nzhead d)); [|unfold m; revert Hd; case nzhead].
+Qed.
+
+Lemma del_head_nb_digits d : del_head (nb_digits d) d = Nil.
+Proof.
+  apply to_list_inj.
+  rewrite nb_digits_spec, del_head_spec_small; [|now simpl].
+  now rewrite List.skipn_all.
+Qed.
+
+Lemma del_tail_nb_digits d : del_tail (nb_digits d) d = Nil.
+Proof. now unfold del_tail; rewrite <-nb_digits_rev, del_head_nb_digits. Qed.
+
+Lemma del_head_app n d d' :
+  n <= nb_digits d -> del_head n (app d d') = app (del_head n d) d'.
+Proof.
+  rewrite nb_digits_spec; intro Hn.
+  apply to_list_inj.
+  rewrite del_head_spec_small.
+  2:{ now rewrite app_spec, List.app_length; apply le_plus_trans. }
+  rewrite !app_spec, (del_head_spec_small _ _ Hn).
+  rewrite List.skipn_app.
+  now rewrite (proj2 (Nat.sub_0_le _ _) Hn).
+Qed.
+
+Lemma del_tail_app n d d' :
+  n <= nb_digits d' -> del_tail n (app d d') = app d (del_tail n d').
+Proof.
+  rewrite nb_digits_spec; intro Hn.
+  unfold del_tail.
+  rewrite <-(of_list_to_list (rev (app d d'))), rev_spec, app_spec.
+  rewrite List.rev_app_distr, <-!rev_spec, <-app_spec, of_list_to_list.
+  rewrite del_head_app; [|now rewrite nb_digits_spec, rev_spec, List.rev_length].
+  apply to_list_inj.
+  rewrite rev_spec, !app_spec, !rev_spec.
+  now rewrite List.rev_app_distr, List.rev_involutive.
+Qed.
+
+Lemma del_tail_app_int n d d' :
+  n <= nb_digits d' -> del_tail_int n (app_int d d') = app_int d (del_tail n d').
+Proof. now case d as [d|d]; simpl; intro H; rewrite del_tail_app. Qed.
+
+Lemma app_del_tail_head n (d:uint) :
+  n <= nb_digits d -> app (del_tail n d) (del_head (nb_digits d - n) d) = d.
+Proof.
+  rewrite nb_digits_spec; intro Hn; unfold del_tail.
+  rewrite <-(of_list_to_list (app _ _)), app_spec, rev_spec.
+  rewrite del_head_spec_small; [|now rewrite rev_spec, List.rev_length].
+  rewrite del_head_spec_small; [|now apply Nat.le_sub_l].
+  rewrite rev_spec.
+  set (n' := _ - n).
+  assert (Hn' : n = length (to_list d) - n').
+  { now apply plus_minus; rewrite  Nat.add_comm; symmetry; apply le_plus_minus_r. }
+  now rewrite Hn', <-List.firstn_skipn_rev, List.firstn_skipn, of_list_to_list.
 Qed.
 
 Lemma app_int_del_tail_head n (d:int) :
-  let ad := match d with Pos d | Neg d => d end in
-  n <= nb_digits ad ->
-  app_int (del_tail_int n d) (del_head (nb_digits ad - n) ad) = d.
+  n <= nb_digits (abs d) ->
+  app_int (del_tail_int n d) (del_head (nb_digits (abs d) - n) (abs d)) = d.
 Proof. now case d; clear d; simpl; intros u Hu; rewrite app_del_tail_head. Qed.
 
+Lemma del_head_app_int_exact i f :
+  nb_digits f < nb_digits (unorm (app (abs i) f)) ->
+  del_head (nb_digits (unorm (app (abs i) f)) - nb_digits f) (unorm (app (abs i) f)) = f.
+Proof.
+  simpl; intro Hnb; generalize Hnb; rewrite (unorm_app_l _ _ Hnb); clear Hnb.
+  replace (_ - _) with (nb_digits (unorm (abs i))).
+  - now rewrite del_head_app; [rewrite del_head_nb_digits|].
+  - rewrite !nb_digits_spec, app_spec, List.app_length.
+    now rewrite Nat.add_comm, minus_plus.
+Qed.
+
+Lemma del_tail_app_int_exact i f :
+  nb_digits f < nb_digits (unorm (app (abs i) f)) ->
+  del_tail_int (nb_digits f) (norm (app_int i f)) = norm i.
+Proof.
+  simpl; intro Hnb.
+  rewrite (norm_app_int _ _ Hnb).
+  rewrite del_tail_app_int; [|now simpl].
+  now rewrite del_tail_nb_digits, app_int_nil_r.
+Qed.
+
 (** Normalization on little-endian numbers *)
 
 Fixpoint nztail d :=
@@ -224,10 +474,13 @@ Proof.
   apply nzhead_revapp.
 Qed.
 
+Lemma rev_rev d : rev (rev d) = d.
+Proof. now apply to_list_inj; rewrite !rev_spec, List.rev_involutive. Qed.
+
 Lemma rev_nztail_rev d :
   rev (nztail (rev d)) = nzhead d.
 Proof.
-  destruct (uint_dec (nztail (rev d)) Nil) as [H|H].
+  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.
@@ -278,21 +531,9 @@ 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 del_head_nonnil n u :
   n < nb_digits u -> del_head n u <> Nil.
 Proof.
@@ -311,73 +552,78 @@ Proof.
   now apply del_head_nonnil.
 Qed.
 
-Lemma nzhead_invol d : nzhead (nzhead d) = nzhead d.
+Lemma nzhead_involutive d : nzhead (nzhead d) = nzhead d.
 Proof.
   now induction d.
 Qed.
+#[deprecated(since="8.13",note="Use nzhead_involutive instead.")]
+Notation nzhead_invol := nzhead_involutive (only parsing).
 
-Lemma nztail_invol d : nztail (nztail d) = nztail d.
+Lemma nztail_involutive 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.
+  now rewrite !rev_nztail_rev, nzhead_involutive.
 Qed.
+#[deprecated(since="8.13",note="Use nztail_involutive instead.")]
+Notation nztail_invol := nztail_involutive (only parsing).
 
-Lemma unorm_invol d : unorm (unorm d) = unorm d.
+Lemma unorm_involutive d : unorm (unorm d) = unorm d.
 Proof.
   unfold unorm.
   destruct (nzhead d) eqn:E; trivial.
   destruct (nzhead_nonzero _ _ E).
 Qed.
+#[deprecated(since="8.13",note="Use unorm_involutive instead.")]
+Notation unorm_invol := unorm_involutive (only parsing).
 
-Lemma norm_invol d : norm (norm d) = norm d.
+Lemma norm_involutive d : norm (norm d) = norm d.
 Proof.
   unfold norm.
   destruct d.
-  - f_equal. apply unorm_invol.
+  - f_equal. apply unorm_involutive.
   - destruct (nzhead d) eqn:E; auto.
     destruct (nzhead_nonzero _ _ E).
 Qed.
+#[deprecated(since="8.13",note="Use norm_involutive instead.")]
+Notation norm_invol := norm_involutive (only parsing).
+
+Lemma lnzhead_neq_d0_head l l' : ~(lnzhead l = cons d0 l').
+Proof. now induction l as [|h t Il]; [|case h]. Qed.
+
+Lemma lnzhead_head_nd0 h t : h <> d0 -> lnzhead (cons h t) = cons h t.
+Proof. now case h. Qed.
 
 Lemma nzhead_del_tail_nzhead_eq n u :
   nzhead u = u ->
   n < nb_digits u ->
   nzhead (del_tail n u) = del_tail n u.
 Proof.
+  rewrite nb_digits_spec, <-List.rev_length.
   intros Hu Hn.
-  assert (Hhd : forall u,
-             nzhead u = u <-> match nth 0 u with D0 _ => False | _ => True end).
-  { clear n u Hu Hn; intro u.
-    case u; clear u; [|intro u..]; [now simpl| |now simpl..]; simpl.
-    split; [|now simpl].
-    apply nzhead_nonzero. }
-  assert (Hhd' : nth 0 (del_tail n u) = nth 0 u).
-  { rewrite <-(app_del_tail_head _ _ (le_Sn_le _ _ Hn)) at 2.
-    unfold app.
-    rewrite nth_revapp_l.
-    - rewrite <-(nth_revapp_l _ _ Nil).
-      + now fold (rev (rev (del_tail n u))); rewrite rev_rev.
-      + unfold del_tail; rewrite rev_rev.
-        rewrite nb_digits_del_head; rewrite nb_digits_rev.
-        * now rewrite <-Nat.lt_add_lt_sub_r.
-        * now apply Nat.lt_le_incl.
-    - unfold del_tail; rewrite rev_rev.
-      rewrite nb_digits_del_head; rewrite nb_digits_rev.
-      + now rewrite <-Nat.lt_add_lt_sub_r.
-      + now apply Nat.lt_le_incl. }
-  revert Hu; rewrite Hhd; intro Hu.
-  now rewrite Hhd, Hhd'.
+  apply to_list_inj; unfold del_tail.
+  rewrite nzhead_spec, rev_spec.
+  rewrite del_head_spec_small; [|now rewrite rev_spec; apply Nat.lt_le_incl].
+  rewrite rev_spec.
+  rewrite List.skipn_rev, List.rev_involutive.
+  generalize (f_equal to_list Hu) Hn; rewrite nzhead_spec; intro Hu'.
+  case (to_list u) as [|h t].
+  { simpl; intro H; exfalso; revert H; apply le_not_lt, Peano.le_0_n. }
+  intro Hn'; generalize (Nat.sub_gt _ _ Hn'); rewrite List.rev_length.
+  case (_ - _); [now simpl|]; intros n' _.
+  rewrite List.firstn_cons, lnzhead_head_nd0; [now simpl|].
+  intro Hh; revert Hu'; rewrite Hh; apply lnzhead_neq_d0_head.
 Qed.
 
 Lemma nzhead_del_tail_nzhead n u :
   n < nb_digits (nzhead u) ->
   nzhead (del_tail n (nzhead u)) = del_tail n (nzhead u).
-Proof. apply nzhead_del_tail_nzhead_eq, nzhead_invol. Qed.
+Proof. apply nzhead_del_tail_nzhead_eq, nzhead_involutive. Qed.
 
 Lemma unorm_del_tail_unorm n u :
   n < nb_digits (unorm u) ->
   unorm (del_tail n (unorm u)) = del_tail n (unorm u).
 Proof.
-  case (uint_dec (nzhead u) Nil).
+  case (uint_eq_dec (nzhead u) Nil).
   - unfold unorm; intros->; case n; [now simpl|]; intro n'.
     now simpl; intro H; exfalso; generalize (lt_S_n _ _ H).
   - unfold unorm.
@@ -396,7 +642,7 @@ Lemma norm_del_tail_int_norm n d :
 Proof.
   case d; clear d; intros u; simpl.
   - now intro H; simpl; rewrite unorm_del_tail_unorm.
-  - case (uint_dec (nzhead u) Nil); intro Hu.
+  - case (uint_eq_dec (nzhead u) Nil); intro Hu.
     + now rewrite Hu; case n; [|intros n' Hn'; generalize (lt_S_n _ _ Hn')].
     + set (m := match nzhead u with Nil => Pos zero | _ => _ end).
       replace m with (Neg (nzhead u)); [|now unfold m; revert Hu; case nzhead].
@@ -418,7 +664,7 @@ Proof.
   generalize (nzhead_revapp d d').
   generalize (nzhead_revapp_0 (nztail d) d').
   generalize (nzhead_revapp (nztail d) d').
-  rewrite nztail_invol.
+  rewrite nztail_involutive.
   now case nztail;
     [intros _ H _ H'; rewrite (H eq_refl), (H' eq_refl)
     |intros d'' H _ H' _; rewrite H; [rewrite H'|]..].
@@ -455,5 +701,10 @@ Proof.
        |rewrite H'; unfold r; clear m r H'];
        unfold norm;
        rewrite rev_rev, <-Hd'';
-       rewrite nzhead_revapp; rewrite nztail_invol; [|rewrite Hd'']..].
+       rewrite nzhead_revapp; rewrite nztail_involutive; [|rewrite Hd'']..].
+Qed.
+
+Lemma unorm_app_l_nil d d' : nzhead d = Nil -> unorm (app d d') = unorm d'.
+Proof.
+  now unfold unorm; rewrite <-nzhead_app_nzhead; intros->; rewrite app_nil_l.
 Qed.
diff --git a/theories/Numbers/DecimalN.v b/theories/Numbers/DecimalN.v
index 8bc5c38fb5..a5dd97f24b 100644
--- a/theories/Numbers/DecimalN.v
+++ b/theories/Numbers/DecimalN.v
@@ -74,7 +74,7 @@ Proof.
   destruct (norm d) eqn:Hd; intros [= <-].
   unfold N.to_int. rewrite Unsigned.to_of. f_equal.
   revert Hd; destruct d; simpl.
-  - intros [= <-]. apply unorm_invol.
+  - intros [= <-]. apply unorm_involutive.
   - destruct (nzhead d); now intros [= <-].
 Qed.
 
@@ -93,7 +93,7 @@ Qed.
 
 Lemma of_int_norm d : N.of_int (norm d) = N.of_int d.
 Proof.
-  unfold N.of_int. now rewrite norm_invol.
+  unfold N.of_int. now rewrite norm_involutive.
 Qed.
 
 Lemma of_inj_pos d d' :
diff --git a/theories/Numbers/DecimalNat.v b/theories/Numbers/DecimalNat.v
index 1962ac5d9d..4fee40caa2 100644
--- a/theories/Numbers/DecimalNat.v
+++ b/theories/Numbers/DecimalNat.v
@@ -270,7 +270,7 @@ Proof.
   destruct (norm d) eqn:Hd; intros [= <-].
   unfold Nat.to_int. rewrite Unsigned.to_of. f_equal.
   revert Hd; destruct d; simpl.
-  - intros [= <-]. apply unorm_invol.
+  - intros [= <-]. apply unorm_involutive.
   - destruct (nzhead d); now intros [= <-].
 Qed.
 
@@ -289,7 +289,7 @@ Qed.
 
 Lemma of_int_norm d : Nat.of_int (norm d) = Nat.of_int d.
 Proof.
-  unfold Nat.of_int. now rewrite norm_invol.
+  unfold Nat.of_int. now rewrite norm_involutive.
 Qed.
 
 Lemma of_inj_pos d d' :
diff --git a/theories/Numbers/DecimalQ.v b/theories/Numbers/DecimalQ.v
index c51cced024..2027813eec 100644
--- a/theories/Numbers/DecimalQ.v
+++ b/theories/Numbers/DecimalQ.v
@@ -15,455 +15,413 @@
 
 Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith.
 
-Lemma of_to (q:Q) : forall d, to_decimal q = Some d -> of_decimal d = q.
+Lemma of_IQmake_to_decimal num den :
+  match IQmake_to_decimal num den with
+  | None => True
+  | Some (DecimalExp _ _ _) => False
+  | Some (Decimal i f) => of_decimal (Decimal i f) = IQmake (IZ_of_Z num) den
+  end.
 Proof.
-  cut (match to_decimal q with None => True | Some d => of_decimal d = q end).
-  { now case to_decimal; [intros d <- d' Hd'; injection Hd'; intros ->|]. }
-  destruct q as (num, den).
-  unfold to_decimal; simpl.
-  generalize (DecimalPos.Unsigned.nztail_to_uint den).
-  case Decimal.nztail; intros u n.
-  case u; clear u; [intros; exact I|intros; exact I|intro u|intros; exact I..].
-  case u; clear u; [|intros; exact I..].
-  unfold Pos.of_uint, Pos.of_uint_acc; rewrite N.mul_1_l.
-  case n.
-  - unfold of_decimal, app_int, app, Z.to_int; simpl.
-    intro H; inversion H as (H1); clear H H1.
-    case num; [reflexivity|intro pnum; fold (rev (rev (Pos.to_uint pnum)))..].
-    + rewrite rev_rev; simpl.
-      now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to.
-    + rewrite rev_rev; simpl.
-      now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to.
-  - clear n; intros n H.
-    injection H; clear H; intros ->.
-    case Nat.ltb.
-    + unfold of_decimal.
-      rewrite of_to.
-      apply f_equal2; [|now simpl].
-      unfold app_int, app, Z.to_int; simpl.
-      now case num;
-        [|intro pnum; fold (rev (rev (Pos.to_uint pnum)));
-          rewrite rev_rev; unfold Z.of_int, Z.of_uint;
-          rewrite DecimalPos.Unsigned.of_to..].
-    + unfold of_decimal; case Nat.ltb_spec; intro Hn; simpl.
-      * rewrite nb_digits_del_head; [|now apply Nat.le_sub_l].
-        rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l].
-        rewrite Nat2Z.inj_sub; [|now apply le_Sn_le].
-        rewrite Z.sub_sub_distr, Z.sub_diag; simpl.
-        rewrite <-(of_to num) at 4.
-        now revert Hn; case Z.to_int; clear num; intros pnum Hn; simpl;
-          (rewrite app_del_tail_head; [|now apply le_Sn_le]).
-      * revert Hn.
-        set (anum := match Z.to_int num with Pos i => i | _ => _ end).
-        intro Hn.
-        assert (H : exists l, nb_digits anum = S l).
-        { exists (Nat.pred (nb_digits anum)); apply S_pred_pos.
-          now unfold anum; case num;
-            [apply Nat.lt_0_1|
-             intro pnum; apply nb_digits_pos, Unsigned.to_uint_nonnil..]. }
-        destruct H as (l, Hl); rewrite Hl.
-        assert (H : forall n d, (nb_digits (Nat.iter n D0 d) = n + nb_digits d)%nat).
-        { now intros n'; induction n'; intro d; [|simpl; rewrite IHn']. }
-        rewrite H, Hl.
-        rewrite Nat.add_succ_r, Nat.sub_add; [|now apply le_S_n; rewrite <-Hl].
-        assert (H' : forall n d, Pos.of_uint (Nat.iter n D0 d) = Pos.of_uint d).
-        { now intro n'; induction n'; intro d; [|simpl; rewrite IHn']. }
-        now unfold anum; case num; simpl; [|intro pnum..];
-          unfold app, Z.of_uint; simpl;
-            rewrite H', ?DecimalPos.Unsigned.of_to.
+  unfold IQmake_to_decimal.
+  generalize (Unsigned.nztail_to_uint den).
+  case Decimal.nztail; intros den' e_den'.
+  case den'; [now simpl|now simpl| |now simpl..]; clear den'; intro den'.
+  case den'; [ |now simpl..]; clear den'.
+  case e_den' as [|e_den']; simpl; intro H; injection H; clear H; intros->.
+  { now unfold of_decimal; simpl; rewrite app_int_nil_r, DecimalZ.of_to. }
+  replace (10 ^ _)%positive with (Nat.iter (S e_den') (Pos.mul 10) 1%positive).
+  2:{ induction e_den' as [|n IHn]; [now simpl| ].
+    now rewrite SuccNat2Pos.inj_succ, Pos.pow_succ_r, <-IHn. }
+  case Nat.ltb_spec; intro He_den'.
+  - unfold of_decimal; simpl.
+    rewrite app_int_del_tail_head; [|now apply Nat.lt_le_incl].
+    rewrite DecimalZ.of_to.
+    now rewrite nb_digits_del_head_sub; [|now apply Nat.lt_le_incl].
+  - unfold of_decimal; simpl.
+    rewrite nb_digits_iter_D0.
+    apply f_equal2.
+    + apply f_equal, DecimalZ.to_int_inj.
+      rewrite DecimalZ.to_of.
+      rewrite <-(DecimalZ.of_to num), DecimalZ.to_of.
+      case (Z.to_int num); clear He_den' num; intro num; simpl.
+      * unfold app; simpl.
+        now rewrite unorm_D0, unorm_iter_D0, unorm_involutive.
+      * case (uint_eq_dec (nzhead num) Nil); [|intro Hn].
+        { intros->; simpl; unfold app; simpl.
+          now rewrite unorm_D0, unorm_iter_D0. }
+        replace (match nzhead num with Nil => _ | _ => _ end)
+          with (Neg (nzhead num)); [|now revert Hn; case nzhead].
+        simpl.
+        rewrite nzhead_iter_D0, nzhead_involutive.
+        now revert Hn; case nzhead.
+    + revert He_den'; case nb_digits as [|n]; [now simpl; rewrite Nat.add_0_r|].
+      intro Hn.
+      rewrite Nat.add_succ_r, Nat.add_comm.
+      now rewrite <-le_plus_minus; [|apply le_S_n].
 Qed.
 
-(* normalize without fractional part, for instance norme 12.3e-1 is 123e-2 *)
-Definition dnorme (d:decimal) : decimal :=
-  let '(i, f, e) :=
-    match d with
-    | Decimal i f => (i, f, Pos Nil)
-    | DecimalExp i f e => (i, f, e)
-    end in
-  let i := norm (app_int i f) in
-  let e := norm (Z.to_int (Z.of_int e - Z.of_nat (nb_digits f))) in
-  match e with
-  | Pos zero => Decimal i Nil
-  | _ => DecimalExp i Nil e
+Lemma IZ_of_Z_IZ_to_Z z z' : IZ_to_Z z = Some z' -> IZ_of_Z z' = z.
+Proof. now case z as [| |p|p]; [|intro H; injection H; intros<-..]. Qed.
+
+Lemma of_IQmake_to_decimal' num den :
+  match IQmake_to_decimal' num den with
+  | None => True
+  | Some (DecimalExp _ _ _) => False
+  | Some (Decimal i f) => of_decimal (Decimal i f) = IQmake num den
   end.
+Proof.
+  unfold IQmake_to_decimal'.
+  case_eq (IZ_to_Z num); [intros num' Hnum'|now simpl].
+  generalize (of_IQmake_to_decimal num' den).
+  case IQmake_to_decimal as [d|]; [|now simpl].
+  case d as [i f|]; [|now simpl].
+  now rewrite (IZ_of_Z_IZ_to_Z _ _ Hnum').
+Qed.
+
+Lemma of_to (q:IQ) : forall d, to_decimal q = Some d -> of_decimal d = q.
+Proof.
+  intro d.
+  case q as [num den|q q'|q q']; simpl.
+  - generalize (of_IQmake_to_decimal' num den).
+    case IQmake_to_decimal' as [d'|]; [|now simpl].
+    case d' as [i f|]; [|now simpl].
+    now intros H H'; injection H'; clear H'; intros <-.
+  - case q as [num den| |]; [|now simpl..].
+    case q' as [num' den'| |]; [|now simpl..].
+    case num' as [z p| | |]; [|now simpl..].
+    case (Z.eq_dec z 10); [intros->|].
+    2:{ case z; [now simpl| |now simpl]; intro pz'.
+      case pz'; [intros d0..| ]; [now simpl| |now simpl].
+      case d0; [intros d1..| ]; [ |now simpl..].
+      case d1; [intros d2..| ]; [now simpl| |now simpl].
+      now case d2. }
+    case (Pos.eq_dec den' 1%positive); [intros->|now case den'].
+    generalize (of_IQmake_to_decimal' num den).
+    case IQmake_to_decimal' as [d'|]; [|now simpl].
+    case d' as [i f|]; [|now simpl].
+    intros <-; clear num den.
+    intros H; injection H; clear H; intros<-.
+    unfold of_decimal; simpl.
+    now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
+  - case q as [num den| |]; [|now simpl..].
+    case q' as [num' den'| |]; [|now simpl..].
+    case num' as [z p| | |]; [|now simpl..].
+    case (Z.eq_dec z 10); [intros->|].
+    2:{ case z; [now simpl| |now simpl]; intro pz'.
+      case pz'; [intros d0..| ]; [now simpl| |now simpl].
+      case d0; [intros d1..| ]; [ |now simpl..].
+      case d1; [intros d2..| ]; [now simpl| |now simpl].
+      now case d2. }
+    case (Pos.eq_dec den' 1%positive); [intros->|now case den'].
+    generalize (of_IQmake_to_decimal' num den).
+    case IQmake_to_decimal' as [d'|]; [|now simpl].
+    case d' as [i f|]; [|now simpl].
+    intros <-; clear num den.
+    intros H; injection H; clear H; intros<-.
+    unfold of_decimal; simpl.
+    now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
+Qed.
 
-(* normalize without exponent part, for instance norme 12.3e-1 is 1.23 *)
-Definition dnormf (d:decimal) : decimal :=
-  match dnorme d with
-  | Decimal i _ => Decimal i Nil
-  | DecimalExp i _ e =>
-    match Z.of_int e with
-    | Z0 => Decimal i Nil
-    | Zpos e => Decimal (norm (app_int i (Pos.iter D0 Nil e))) Nil
-    | Zneg e =>
-      let ne := Pos.to_nat e in
-      let ai := match i with Pos d | Neg d => d end in
-      let ni := nb_digits ai in
-      if ne <? ni then
-        Decimal (del_tail_int ne i) (del_head (ni - ne) ai)
-      else
-        let z := match i with Pos _ => Pos zero | Neg _ => Neg zero end in
-        Decimal z (Nat.iter (ne - ni) D0 ai)
+Definition dnorm (d:decimal) : decimal :=
+  let norm_i i f :=
+    match i with
+    | Pos i => Pos (unorm i)
+    | Neg i => match nzhead (app i f) with Nil => Pos zero | _ => Neg (unorm i) end
+    end in
+  match d with
+  | Decimal i f => Decimal (norm_i i f) f
+  | DecimalExp i f e =>
+    match norm e with
+    | Pos zero => Decimal (norm_i i f) f
+    | e => DecimalExp (norm_i i f) f e
     end
   end.
 
-Lemma dnorme_spec d :
-  match dnorme d with
-  | Decimal i Nil => i = norm i
-  | DecimalExp i Nil e => i = norm i /\ e = norm e /\ e <> Pos zero
-  | _ => False
+Lemma dnorm_spec_i d :
+  let (i, f) :=
+    match d with Decimal i f => (i, f) | DecimalExp i f _ => (i, f) end in
+  let i' := match dnorm d with Decimal i _ => i | DecimalExp i _ _ => i end in
+  match i with
+  | Pos i => i' = Pos (unorm i)
+  | Neg i =>
+    (i' = Neg (unorm i) /\ (nzhead i <> Nil \/ nzhead f <> Nil))
+    \/ (i' = Pos zero /\ (nzhead i = Nil /\ nzhead f = Nil))
   end.
 Proof.
-  case d; clear d; intros i f; [|intro e]; unfold dnorme; simpl.
-  - set (e' := Z.to_int _).
-    case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne'].
-    + now rewrite norm_invol.
-    + set (r := DecimalExp _ _ _).
-      set (m := match norm e' with Pos zero => _ | _ => _ end).
-      replace m with r; [now unfold r; rewrite !norm_invol|].
-      unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
-      now case e''; [|intro e'''; case e'''..].
-  - set (e' := Z.to_int _).
-    case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne'].
-    + now rewrite norm_invol.
-    + set (r := DecimalExp _ _ _).
-      set (m := match norm e' with Pos zero => _ | _ => _ end).
-      replace m with r; [now unfold r; rewrite !norm_invol|].
-      unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
-      now case e''; [|intro e'''; case e'''..].
+  case d as [i f|i f e]; case i as [i|i].
+  - now simpl.
+  - simpl; case (uint_eq_dec (nzhead (app i f)) Nil); intro Ha.
+    + rewrite Ha; right; split; [now simpl|split].
+      * now unfold unorm; rewrite (nzhead_app_nil_l _ _ Ha).
+      * now unfold unorm; rewrite (nzhead_app_nil_r _ _ Ha).
+    + left; split; [now revert Ha; case nzhead|].
+      case (uint_eq_dec (nzhead i) Nil).
+      * intro Hi; right; intro Hf; apply Ha.
+        now rewrite <-nzhead_app_nzhead, Hi, app_nil_l.
+      * now intro H; left.
+  - simpl; case (norm e); clear e; intro e; [|now simpl].
+    now case e; clear e; [|intro e..]; [|case e|..].
+  - simpl.
+    set (m := match nzhead _ with Nil => _ | _ => _ end).
+    set (m' := match _ with Decimal _ _ => _ | _ => _ end).
+    replace m' with m.
+    2:{ unfold m'; case (norm e); clear m' e; intro e; [|now simpl].
+      now case e; clear e; [|intro e..]; [|case e|..]. }
+    unfold m; case (uint_eq_dec (nzhead (app i f)) Nil); intro Ha.
+    + rewrite Ha; right; split; [now simpl|split].
+      * now unfold unorm; rewrite (nzhead_app_nil_l _ _ Ha).
+      * now unfold unorm; rewrite (nzhead_app_nil_r _ _ Ha).
+    + left; split; [now revert Ha; case nzhead|].
+      case (uint_eq_dec (nzhead i) Nil).
+      * intro Hi; right; intro Hf; apply Ha.
+        now rewrite <-nzhead_app_nzhead, Hi, app_nil_l.
+      * now intro H; left.
+Qed.
+
+Lemma dnorm_spec_f d :
+  let f := match d with Decimal _ f => f | DecimalExp _ f _ => f end in
+  let f' := match dnorm d with Decimal _ f => f | DecimalExp _ f _ => f end in
+  f' = f.
+Proof.
+  case d as [i f|i f e]; [now simpl|].
+  simpl; case (int_eq_dec (norm e) (Pos zero)); [now intros->|intro He].
+  set (i' := match i with Pos _ => _ | _ => _ end).
+  set (m := match norm e with Pos Nil => _ | _ => _ end).
+  replace m with (DecimalExp i' f (norm e)); [now simpl|].
+  unfold m; revert He; case (norm e); clear m e; intro e; [|now simpl].
+  now case e; clear e; [|intro e; case e|..].
 Qed.
 
-Lemma dnormf_spec d :
-  match dnormf d with
-  | Decimal i f => i = Neg zero \/ i = norm i
-  | _ => False
+Lemma dnorm_spec_e d :
+  match d, dnorm d with
+    | Decimal _ _, Decimal _ _ => True
+    | DecimalExp _ _ e, Decimal _ _ => norm e = Pos zero
+    | DecimalExp _ _ e, DecimalExp _ _ e' => e' = norm e /\ e' <> Pos zero
+    | Decimal _ _, DecimalExp _ _ _ => False
   end.
 Proof.
-  case d; clear d; intros i f; [|intro e]; unfold dnormf, dnorme; simpl.
-  - set (e' := Z.to_int _).
-    case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne'].
-    + now right; rewrite norm_invol.
-    + set (r := DecimalExp _ _ _).
-      set (m := match norm e' with Pos zero => _ | _ => _ end).
-      assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
-      { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
-        now case e''; [|intro e'''; case e'''..]. }
-      rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-      case_eq (Z.of_int e'); [|intros pe'..]; intro Hpe';
-        [now right; rewrite norm_invol..|].
-      case Nat.ltb_spec.
-      * now intro H; rewrite (norm_del_tail_int_norm _ _ H); right.
-      * now intros _; case norm; intros _; [right|left].
-  - set (e' := Z.to_int _).
-    case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne'].
-    + now right; rewrite norm_invol.
-    + set (r := DecimalExp _ _ _).
-      set (m := match norm e' with Pos zero => _ | _ => _ end).
-      assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
-      { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
-        now case e''; [|intro e'''; case e'''..]. }
-      rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-      case_eq (Z.of_int e'); [|intros pe'..]; intro Hpe';
-        [now right; rewrite norm_invol..|].
-      case Nat.ltb_spec.
-      * now intro H; rewrite (norm_del_tail_int_norm _ _ H); right.
-      * now intros _; case norm; intros _; [right|left].
+  case d as [i f|i f e]; [now simpl|].
+  simpl; case (int_eq_dec (norm e) (Pos zero)); [now intros->|intro He].
+  set (i' := match i with Pos _ => _ | _ => _ end).
+  set (m := match norm e with Pos Nil => _ | _ => _ end).
+  replace m with (DecimalExp i' f (norm e)); [now simpl|].
+  unfold m; revert He; case (norm e); clear m e; intro e; [|now simpl].
+  now case e; clear e; [|intro e; case e|..].
 Qed.
 
-Lemma dnorme_invol d : dnorme (dnorme d) = dnorme d.
+Lemma dnorm_involutive d : dnorm (dnorm d) = dnorm d.
 Proof.
-  case d; clear d; intros i f; [|intro e]; unfold dnorme; simpl.
-  - set (e' := Z.to_int _).
-    case (int_eq_dec (norm e') (Pos zero)); intro Hne'.
-    + rewrite Hne'; simpl; rewrite app_int_nil_r, norm_invol.
-      revert Hne'.
-      rewrite <-to_of.
-      change (Pos zero) with (Z.to_int 0).
-      intro H; generalize (to_int_inj _ _ H); clear H.
-      unfold e'; rewrite DecimalZ.of_to.
-      now case f; [rewrite app_int_nil_r|..].
-    + set (r := DecimalExp _ _ _).
-      set (m := match norm e' with Pos zero => _ | _ => _ end).
-      assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
-      { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
-        now case e''; [|intro e'''; case e'''..]. }
-      rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-      unfold nb_digits, Z.of_nat; rewrite Z.sub_0_r, to_of, norm_invol.
-      rewrite app_int_nil_r, norm_invol.
-      set (r := DecimalExp _ _ _).
-      set (m := match norm e' with Pos zero => _ | _ => _ end).
-      unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
-      now case e''; [|intro e'''; case e'''..].
-  - set (e' := Z.to_int _).
-    case (int_eq_dec (norm e') (Pos zero)); intro Hne'.
-    + rewrite Hne'; simpl; rewrite app_int_nil_r, norm_invol.
-      revert Hne'.
-      rewrite <-to_of.
-      change (Pos zero) with (Z.to_int 0).
-      intro H; generalize (to_int_inj _ _ H); clear H.
-      unfold e'; rewrite DecimalZ.of_to.
-      now case f; [rewrite app_int_nil_r|..].
-    + set (r := DecimalExp _ _ _).
-      set (m := match norm e' with Pos zero => _ | _ => _ end).
-      assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
-      { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
-        now case e''; [|intro e'''; case e'''..]. }
-      rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-      unfold nb_digits, Z.of_nat; rewrite Z.sub_0_r, to_of, norm_invol.
-      rewrite app_int_nil_r, norm_invol.
-      set (r := DecimalExp _ _ _).
-      set (m := match norm e' with Pos zero => _ | _ => _ end).
-      unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
-      now case e''; [|intro e'''; case e'''..].
+  case d as [i f|i f e]; case i as [i|i].
+  - now simpl; rewrite unorm_involutive.
+  - simpl; case (uint_eq_dec (nzhead (app i f)) Nil); [now intros->|intro Ha].
+    set (m := match nzhead _ with Nil =>_ | _ => _ end).
+    replace m with (Neg (unorm i)).
+    2:{ now unfold m; revert Ha; case nzhead. }
+    case (uint_eq_dec (nzhead i) Nil); intro Hi.
+    + unfold unorm; rewrite Hi; simpl.
+      case (uint_eq_dec (nzhead f) Nil).
+      * intro Hf; exfalso; apply Ha.
+        now rewrite <-nzhead_app_nzhead, Hi, app_nil_l.
+      * now case nzhead.
+    + rewrite unorm_involutive, (unorm_nzhead _ Hi), nzhead_app_nzhead.
+      now revert Ha; case nzhead.
+  - simpl; case (int_eq_dec (norm e) (Pos zero)); intro He.
+    + now rewrite He; simpl; rewrite unorm_involutive.
+    + set (m := match norm e with Pos Nil => _ | _ => _ end).
+      replace m with (DecimalExp (Pos (unorm i)) f (norm e)).
+      2:{ unfold m; revert He; case (norm e); clear m e; intro e; [|now simpl].
+        now case e; clear e; [|intro e; case e|..]. }
+      simpl; rewrite norm_involutive, unorm_involutive.
+      revert He; case (norm e); clear m e; intro e; [|now simpl].
+      now case e; clear e; [|intro e; case e|..].
+  - simpl; case (int_eq_dec (norm e) (Pos zero)); intro He.
+    + rewrite He; simpl.
+      case (uint_eq_dec (nzhead (app i f)) Nil); [now intros->|intro Ha].
+      set (m := match nzhead _ with Nil =>_ | _ => _ end).
+      replace m with (Neg (unorm i)).
+      2:{ now unfold m; revert Ha; case nzhead. }
+      case (uint_eq_dec (nzhead i) Nil); intro Hi.
+      * unfold unorm; rewrite Hi; simpl.
+        case (uint_eq_dec (nzhead f) Nil).
+        -- intro Hf; exfalso; apply Ha.
+           now rewrite <-nzhead_app_nzhead, Hi, app_nil_l.
+        -- now case nzhead.
+      * rewrite unorm_involutive, (unorm_nzhead _ Hi), nzhead_app_nzhead.
+        now revert Ha; case nzhead.
+    + set (m := match norm e with Pos Nil => _ | _ => _ end).
+      pose (i' := match nzhead (app i f) with Nil => Pos zero | _ => Neg (unorm i) end).
+      replace m with (DecimalExp i' f (norm e)).
+      2:{ unfold m; revert He; case (norm e); clear m e; intro e; [|now simpl].
+        now case e; clear e; [|intro e; case e|..]. }
+      simpl; rewrite norm_involutive.
+      set (i'' := match i' with Pos _ => _ | _ => _ end).
+      clear m; set (m := match norm e with Pos Nil => _ | _ => _ end).
+      replace m with (DecimalExp i'' f (norm e)).
+      2:{ unfold m; revert He; case (norm e); clear m e; intro e; [|now simpl].
+        now case e; clear e; [|intro e; case e|..]. }
+      unfold i'', i'.
+      case (uint_eq_dec (nzhead (app i f)) Nil); [now intros->|intro Ha].
+      fold i'; replace i' with (Neg (unorm i)).
+      2:{ now unfold i'; revert Ha; case nzhead. }
+      case (uint_eq_dec (nzhead i) Nil); intro Hi.
+      * unfold unorm; rewrite Hi; simpl.
+        case (uint_eq_dec (nzhead f) Nil).
+        -- intro Hf; exfalso; apply Ha.
+           now rewrite <-nzhead_app_nzhead, Hi, app_nil_l.
+        -- now case nzhead.
+      * rewrite unorm_involutive, (unorm_nzhead _ Hi), nzhead_app_nzhead.
+        now revert Ha; case nzhead.
 Qed.
 
-Lemma dnormf_invol d : dnormf (dnormf d) = dnormf d.
+Lemma IZ_to_Z_IZ_of_Z z : IZ_to_Z (IZ_of_Z z) = Some z.
+Proof. now case z. Qed.
+
+Lemma dnorm_i_exact i f :
+  (nb_digits f < nb_digits (unorm (app (abs i) f)))%nat ->
+  match i with
+  | Pos i => Pos (unorm i)
+  | Neg i =>
+    match nzhead (app i f) with
+    | Nil => Pos zero
+    | _ => Neg (unorm i)
+    end
+  end = norm i.
 Proof.
-  case d; clear d; intros i f; [|intro e]; unfold dnormf, dnorme; simpl.
-  - set (e' := Z.to_int _).
-    case (int_eq_dec (norm e') (Pos zero)); intro Hne'.
-    + rewrite Hne'; simpl; rewrite app_int_nil_r, norm_invol.
-      revert Hne'.
-      rewrite <-to_of.
-      change (Pos zero) with (Z.to_int 0).
-      intro H; generalize (to_int_inj _ _ H); clear H.
-      unfold e'; rewrite DecimalZ.of_to.
-      now case f; [rewrite app_int_nil_r|..].
-    + set (r := DecimalExp _ _ _).
-      set (m := match norm e' with Pos zero => _ | _ => _ end).
-      assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
-      { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
-        now case e''; [|intro e'''; case e'''..]. }
-      rewrite of_int_norm.
-      case_eq (Z.of_int e'); [|intro pe'..]; intro Hnpe';
-        [now simpl; rewrite app_int_nil_r, norm_invol..|].
-      case Nat.ltb_spec; intro Hpe'.
-      * rewrite nb_digits_del_head; [|now apply Nat.le_sub_l].
-        rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l].
-        rewrite Nat2Z.inj_sub; [|now apply Nat.lt_le_incl].
-        simpl.
-        rewrite Z.sub_sub_distr, Z.sub_diag, Z.add_0_l.
-        rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-        rewrite positive_nat_Z; simpl.
-        unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
-        rewrite app_int_del_tail_head; [|now apply Nat.lt_le_incl].
-        now rewrite norm_invol, (proj2 (Nat.ltb_lt _ _) Hpe').
-      * simpl.
-        rewrite nb_digits_iter_D0.
-        rewrite (Nat.sub_add _ _ Hpe').
-        rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-        rewrite positive_nat_Z; simpl.
-        unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
-        revert Hpe'.
-        set (i' := norm (app_int i f)).
-        case_eq i'; intros u Hu Hpe'.
-        ++ simpl; unfold app; simpl.
-           rewrite unorm_D0, unorm_iter_D0.
-           assert (Hu' : unorm u = u).
-           { generalize (f_equal norm Hu).
-             unfold i'; rewrite norm_invol; fold i'.
-             now simpl; rewrite Hu; intro H; injection H. }
-           now rewrite Hu', (proj2 (Nat.ltb_ge _ _) Hpe').
-        ++ simpl; rewrite nzhead_iter_D0.
-           assert (Hu' : nzhead u = u).
-           { generalize (f_equal norm Hu).
-             unfold i'; rewrite norm_invol; fold i'.
-             now rewrite Hu; simpl; case (nzhead u); [|intros u' H; injection H..]. }
-           rewrite Hu'.
-           assert (Hu'' : u <> Nil).
-           { intro H; revert Hu; rewrite H; unfold i'.
-             now case app_int; intro u'; [|simpl; case nzhead]. }
-           set (m := match u with Nil => Pos zero | _ => _ end).
-           assert (H : m = Neg u); [|rewrite H; clear m H].
-           { now revert Hu''; unfold m; case u. }
-           now rewrite (proj2 (Nat.ltb_ge _ _) Hpe').
-  - set (e' := Z.to_int _).
-    case (int_eq_dec (norm e') (Pos zero)); intro Hne'.
-    + rewrite Hne'; simpl; rewrite app_int_nil_r, norm_invol.
-      revert Hne'.
-      rewrite <-to_of.
-      change (Pos zero) with (Z.to_int 0).
-      intro H; generalize (to_int_inj _ _ H); clear H.
-      unfold e'; rewrite DecimalZ.of_to.
-      now case f; [rewrite app_int_nil_r|..].
-    + set (r := DecimalExp _ _ _).
-      set (m := match norm e' with Pos zero => _ | _ => _ end).
-      assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
-      { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
-        now case e''; [|intro e'''; case e'''..]. }
-      rewrite of_int_norm.
-      case_eq (Z.of_int e'); [|intro pe'..]; intro Hnpe';
-        [now simpl; rewrite app_int_nil_r, norm_invol..|].
-      case Nat.ltb_spec; intro Hpe'.
-      * rewrite nb_digits_del_head; [|now apply Nat.le_sub_l].
-        rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l].
-        rewrite Nat2Z.inj_sub; [|now apply Nat.lt_le_incl].
-        simpl.
-        rewrite Z.sub_sub_distr, Z.sub_diag, Z.add_0_l.
-        rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-        rewrite positive_nat_Z; simpl.
-        unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
-        rewrite app_int_del_tail_head; [|now apply Nat.lt_le_incl].
-        now rewrite norm_invol, (proj2 (Nat.ltb_lt _ _) Hpe').
-      * simpl.
-        rewrite nb_digits_iter_D0.
-        rewrite (Nat.sub_add _ _ Hpe').
-        rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-        rewrite positive_nat_Z; simpl.
-        unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
-        revert Hpe'.
-        set (i' := norm (app_int i f)).
-        case_eq i'; intros u Hu Hpe'.
-        ++ simpl; unfold app; simpl.
-           rewrite unorm_D0, unorm_iter_D0.
-           assert (Hu' : unorm u = u).
-           { generalize (f_equal norm Hu).
-             unfold i'; rewrite norm_invol; fold i'.
-             now simpl; rewrite Hu; intro H; injection H. }
-           now rewrite Hu', (proj2 (Nat.ltb_ge _ _) Hpe').
-        ++ simpl; rewrite nzhead_iter_D0.
-           assert (Hu' : nzhead u = u).
-           { generalize (f_equal norm Hu).
-             unfold i'; rewrite norm_invol; fold i'.
-             now rewrite Hu; simpl; case (nzhead u); [|intros u' H; injection H..]. }
-           rewrite Hu'.
-           assert (Hu'' : u <> Nil).
-           { intro H; revert Hu; rewrite H; unfold i'.
-             now case app_int; intro u'; [|simpl; case nzhead]. }
-           set (m := match u with Nil => Pos zero | _ => _ end).
-           assert (H : m = Neg u); [|rewrite H; clear m H].
-           { now revert Hu''; unfold m; case u. }
-           now rewrite (proj2 (Nat.ltb_ge _ _) Hpe').
+  case i as [ni|ni]; [now simpl|]; simpl.
+  case (uint_eq_dec (nzhead (app ni f)) Nil); intro Ha.
+  { now rewrite Ha, (nzhead_app_nil_l _ _ Ha). }
+  rewrite (unorm_nzhead _ Ha).
+  set (m := match nzhead _ with Nil => _ | _ => _ end).
+  replace m with (Neg (unorm ni)); [|now unfold m; revert Ha; case nzhead].
+  case (uint_eq_dec (nzhead ni) Nil); intro Hni.
+  { rewrite <-nzhead_app_nzhead, Hni, app_nil_l.
+    intro H; exfalso; revert H; apply le_not_lt, nb_digits_nzhead. }
+  clear m; set (m := match nzhead ni with Nil => _ | _ => _ end).
+  replace m with (Neg (nzhead ni)); [|now unfold m; revert Hni; case nzhead].
+  now rewrite (unorm_nzhead _ Hni).
+Qed.
+
+Lemma dnorm_i_exact' i f :
+  (nb_digits (unorm (app (abs i) f)) <= nb_digits f)%nat ->
+  match i with
+  | Pos i => Pos (unorm i)
+  | Neg i =>
+    match nzhead (app i f) with
+    | Nil => Pos zero
+    | _ => Neg (unorm i)
+    end
+  end =
+  match norm (app_int i f) with
+  | Pos _ => Pos zero
+  | Neg _ => Neg zero
+  end.
+Proof.
+  case i as [ni|ni]; simpl.
+  { now intro Hnb; rewrite (unorm_app_zero _ _ Hnb). }
+  unfold unorm.
+  case (uint_eq_dec (nzhead (app ni f)) Nil); intro Hn.
+  { now rewrite Hn. }
+  set (m := match nzhead _ with Nil => _ | _ => _ end).
+  replace m with (nzhead (app ni f)).
+  2:{ now unfold m; revert Hn; case nzhead. }
+  clear m; set (m := match nzhead _ with Nil => _ | _ => _ end).
+  replace m with (Neg (unorm ni)).
+  2:{ now unfold m, unorm; revert Hn; case nzhead. }
+  clear m; set (m := match nzhead _ with Nil => _ | _ => _ end).
+  replace m with (Neg (nzhead (app ni f))).
+  2:{ now unfold m; revert Hn; case nzhead. }
+  rewrite <-(unorm_nzhead _ Hn).
+  now intro H; rewrite (unorm_app_zero _ _ H).
 Qed.
 
-Lemma to_of (d:decimal) :
-  to_decimal (of_decimal d) = Some (dnorme d)
-  \/ to_decimal (of_decimal d) = Some (dnormf d).
+Lemma to_of (d:decimal) : to_decimal (of_decimal d) = Some (dnorm d).
 Proof.
-  unfold to_decimal.
-  pose (t10 := fun y => ((y + y~0~0)~0)%positive).
-  assert (H : exists e_den,
-             Decimal.nztail (Pos.to_uint (Qden (of_decimal d))) = (D1 Nil, e_den)).
-  { assert (H : forall p,
-               Decimal.nztail (Pos.to_uint (Pos.iter t10 1%positive p))
-               = (D1 Nil, Pos.to_nat p)).
-    { intro p; rewrite Pos2Nat.inj_iter.
-      fold (Nat.iter (Pos.to_nat p) t10 1%positive).
-      induction (Pos.to_nat p); [now simpl|].
-      rewrite DecimalPos.Unsigned.nat_iter_S.
-      unfold Pos.to_uint.
-      change (Pos.to_little_uint _)
-        with (Unsigned.to_lu (10 * N.pos (Nat.iter n t10 1%positive))).
-      rewrite Unsigned.to_ldec_tenfold.
-      revert IHn; unfold Pos.to_uint.
-      unfold Decimal.nztail; rewrite !rev_rev; simpl.
-      set (f'' := _ (Pos.to_little_uint _)).
-      now case f''; intros r n' H; inversion H. }
-    case d; intros i f; [|intro e]; unfold of_decimal; simpl.
-    - case (- Z.of_nat _)%Z; [|intro p..]; simpl; [now exists O..|].
-      exists (Pos.to_nat p); apply H.
-    - case (_ - _)%Z; [|intros p..]; simpl; [now exists O..|].
-      exists (Pos.to_nat p); apply H. }
-  generalize (DecimalPos.Unsigned.nztail_to_uint (Qden (of_decimal d))).
-  destruct H as (e, He); rewrite He; clear He; simpl.
-  assert (Hn1 : forall p, N.pos (Pos.iter t10 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 (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 10 (Z.pos n)).
-    change (Z.pos (t10 m)) with (Z.mul 10 (Z.pos m)).
-    rewrite Z.mul_comm, (Z.mul_comm 10).
-    intro H; generalize (f_equal (fun z => Z.div z 10) H); clear H.
-    now rewrite !Z.div_mul; [|now simpl..]; intro H; inversion H. }
-  assert (Hinj : forall n m,
-             Nat.iter n t10 1%positive = Nat.iter m t10 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 (Ht10inj _ _ H); clear H; intro H.
-    now rewrite (IHn _ H). }
-  case e; clear e; [|intro e]; simpl; unfold of_decimal, dnormf, dnorme.
-  - case d; clear d; intros i f; [|intro e]; simpl.
-    + intro H; left; revert H.
-      generalize (nb_digits_pos f).
-      case f;
-        [|now clear f; intro f; intros H1 H2; exfalso; revert H1 H2;
-          case nb_digits; simpl;
-          [intros H _; apply (lt_irrefl O), H|intros n _; apply Hn1]..].
-      now intros _ _; simpl; rewrite to_of.
-    + intro H; right; revert H.
-      rewrite <-to_of, DecimalZ.of_to.
-      set (emf := (_ - _)%Z).
-      case_eq emf; [|intro pemf..].
-      * now simpl; rewrite to_of.
-      * set (r := DecimalExp _ _ _).
-        set (m := match _ with Pos _ => _ | _ => r end).
-        assert (H : m = r).
-        { unfold m, Z.to_int.
-          generalize (Unsigned.to_uint_nonzero pemf).
-          now case Pos.to_uint; [|intro u; case u..]. }
-        rewrite H; unfold r; clear H m r.
-        rewrite DecimalZ.of_to.
-        simpl Qnum.
-        intros Hpemf _.
-        apply f_equal; apply f_equal2; [|reflexivity].
-        rewrite !Pos2Nat.inj_iter.
-        set (n := _ pemf).
-        fold (Nat.iter n (Z.mul 10) (Z.of_int (app_int i f))).
-        fold (Nat.iter n D0 Nil).
-        rewrite <-of_int_iter_D0, to_of.
-        now rewrite norm_app_int_norm; [|induction n].
-      * 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.
-      simpl Qden.
-      intro H; injection H; clear H; unfold Pos.pow.
-      rewrite !Pos2Nat.inj_iter.
-      intro H; generalize (Hinj _ _ H); clear H; intro H.
-      generalize (SuccNat2Pos.inj _ _ ((Pos2Nat.inj _ _ H))); clear H.
-      intro He; rewrite <-He; clear e He.
-      simpl Qnum.
-      case Nat.ltb; [left|right].
-      * now rewrite <-to_of, DecimalZ.of_to, to_of.
-      * rewrite to_of.
-        set (nif := norm _).
-        set (anif := match nif with Pos i0 => i0 | _ => _ end).
-        set (r := DecimalExp nif Nil _).
-        set (m := match _ with Pos _ => _ | _ => r end).
-        assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
-        { now unfold m; rewrite <-to_of, DecimalZ.of_to. }
-        rewrite <-to_of, !DecimalZ.of_to.
-        fold anif.
-        now rewrite 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.
-      simpl 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.
-      intro H; revert Hpnemf; rewrite H; clear pnemf H; intro Hnemf.
-      simpl Qnum.
-      case Nat.ltb; [left|right].
-      * now rewrite <-to_of, DecimalZ.of_to, to_of.
-      * rewrite to_of.
-        set (nif := norm _).
-        set (anif := match nif with Pos i0 => i0 | _ => _ end).
-        set (r := DecimalExp nif Nil _).
-        set (m := match _ with Pos _ => _ | _ => r end).
-        assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
-        { now unfold m; rewrite <-to_of, DecimalZ.of_to. }
-        rewrite <-to_of, !DecimalZ.of_to.
-        fold anif.
-        now rewrite SuccNat2Pos.id_succ.
+  case d as [i f|i f e].
+  - unfold of_decimal; simpl; unfold IQmake_to_decimal'.
+    rewrite IZ_to_Z_IZ_of_Z.
+    unfold IQmake_to_decimal; simpl.
+    change (fun _ : positive => _) with (Pos.mul 10).
+    rewrite nztail_to_uint_pow10, to_of.
+    case_eq (nb_digits f); [|intro nb]; intro Hnb.
+    + rewrite (nb_digits_0 _ Hnb), app_int_nil_r.
+      case i as [ni|ni]; [now simpl|].
+      rewrite app_nil_r; simpl; unfold unorm.
+      now case (nzhead ni).
+    + rewrite <-Hnb.
+      rewrite abs_norm, abs_app_int.
+      case Nat.ltb_spec; intro Hnb'.
+      * rewrite (del_tail_app_int_exact _ _ Hnb').
+        rewrite (del_head_app_int_exact _ _ Hnb').
+        now rewrite (dnorm_i_exact _ _ Hnb').
+      * rewrite (unorm_app_r _ _ Hnb').
+        rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb].
+        now rewrite dnorm_i_exact'.
+  - unfold of_decimal; simpl.
+    rewrite <-to_of.
+    case (Z.of_int e); clear e; [|intro e..]; simpl.
+    + unfold IQmake_to_decimal'.
+      rewrite IZ_to_Z_IZ_of_Z.
+      unfold IQmake_to_decimal; simpl.
+      change (fun _ : positive => _) with (Pos.mul 10).
+      rewrite nztail_to_uint_pow10, to_of.
+      case_eq (nb_digits f); [|intro nb]; intro Hnb.
+      * rewrite (nb_digits_0 _ Hnb), app_int_nil_r.
+        case i as [ni|ni]; [now simpl|].
+        rewrite app_nil_r; simpl; unfold unorm.
+        now case (nzhead ni).
+      * rewrite <-Hnb.
+        rewrite abs_norm, abs_app_int.
+        case Nat.ltb_spec; intro Hnb'.
+        -- rewrite (del_tail_app_int_exact _ _ Hnb').
+           rewrite (del_head_app_int_exact _ _ Hnb').
+           now rewrite (dnorm_i_exact _ _ Hnb').
+        -- rewrite (unorm_app_r _ _ Hnb').
+           rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb].
+           now rewrite dnorm_i_exact'.
+    + unfold IQmake_to_decimal'.
+      rewrite IZ_to_Z_IZ_of_Z.
+      unfold IQmake_to_decimal; simpl.
+      change (fun _ : positive => _) with (Pos.mul 10).
+      rewrite nztail_to_uint_pow10, to_of.
+      generalize (Unsigned.to_uint_nonzero e); intro He.
+      set (dnorm_i := match i with Pos _ => _ | _ => _ end).
+      set (m := match Pos.to_uint e with Nil => _ | _ => _ end).
+      replace m with (DecimalExp dnorm_i f (Pos (Pos.to_uint e))).
+      2:{ now unfold m; revert He; case (Pos.to_uint e); [|intro u; case u|..]. }
+      clear m; unfold dnorm_i.
+      case_eq (nb_digits f); [|intro nb]; intro Hnb.
+      * rewrite (nb_digits_0 _ Hnb), app_int_nil_r.
+        case i as [ni|ni]; [now simpl|].
+        rewrite app_nil_r; simpl; unfold unorm.
+        now case (nzhead ni).
+      * rewrite <-Hnb.
+        rewrite abs_norm, abs_app_int.
+        case Nat.ltb_spec; intro Hnb'.
+        -- rewrite (del_tail_app_int_exact _ _ Hnb').
+           rewrite (del_head_app_int_exact _ _ Hnb').
+           now rewrite (dnorm_i_exact _ _ Hnb').
+        -- rewrite (unorm_app_r _ _ Hnb').
+           rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb].
+           now rewrite dnorm_i_exact'.
+    + unfold IQmake_to_decimal'.
+      rewrite IZ_to_Z_IZ_of_Z.
+      unfold IQmake_to_decimal; simpl.
+      change (fun _ : positive => _) with (Pos.mul 10).
+      rewrite nztail_to_uint_pow10, to_of.
+      case_eq (nb_digits f); [|intro nb]; intro Hnb.
+      * rewrite (nb_digits_0 _ Hnb), app_int_nil_r.
+        case i as [ni|ni]; [now simpl|].
+        rewrite app_nil_r; simpl; unfold unorm.
+        now case (nzhead ni).
+      * rewrite <-Hnb.
+        rewrite abs_norm, abs_app_int.
+        case Nat.ltb_spec; intro Hnb'.
+        -- rewrite (del_tail_app_int_exact _ _ Hnb').
+           rewrite (del_head_app_int_exact _ _ Hnb').
+           now rewrite (dnorm_i_exact _ _ Hnb').
+        -- rewrite (unorm_app_r _ _ Hnb').
+           rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb].
+           now rewrite dnorm_i_exact'.
 Qed.
 
 (** Some consequences *)
@@ -478,84 +436,24 @@ Proof.
   now intros d _ H1 H2; rewrite <-(H1 d eq_refl), <-(H2 d eq_refl).
 Qed.
 
-Lemma to_decimal_surj d :
-  exists q, to_decimal q = Some (dnorme d) \/ to_decimal q = Some (dnormf d).
+Lemma to_decimal_surj d : exists q, to_decimal q = Some (dnorm d).
 Proof.
   exists (of_decimal d). apply to_of.
 Qed.
 
-Lemma of_decimal_dnorme d : of_decimal (dnorme d) = of_decimal d.
+Lemma of_decimal_dnorm d : of_decimal (dnorm d) = of_decimal d.
+Proof. now apply to_decimal_inj; rewrite !to_of; [|rewrite dnorm_involutive]. Qed.
+
+Lemma of_inj d d' : of_decimal d = of_decimal d' -> dnorm d = dnorm d'.
 Proof.
-  unfold of_decimal, dnorme.
-  destruct d.
-  - rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
-    case_eq (nb_digits f); [|intro nf]; intro Hnf.
-    + now simpl; rewrite app_int_nil_r, <-DecimalZ.to_of, DecimalZ.of_to.
-    + simpl; rewrite Z.sub_0_r.
-      unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
-      rewrite app_int_nil_r.
-      now rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-  - rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
-    set (emf := (_ - _)%Z).
-    case_eq emf; [|intro pemf..]; intro Hemf.
-    + now simpl; rewrite app_int_nil_r, <-DecimalZ.to_of, DecimalZ.of_to.
-    + simpl.
-      set (r := DecimalExp _ Nil _).
-      set (m := match Pos.to_uint pemf with zero => _ | _ => r end).
-      assert (H : m = r); [|rewrite H; unfold r; clear m r H].
-      { generalize (Unsigned.to_uint_nonzero pemf).
-        now unfold m; case Pos.to_uint; [|intro u; case u|..]. }
-      simpl; rewrite Z.sub_0_r.
-      unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
-      rewrite app_int_nil_r.
-      now rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-    + simpl.
-      unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
-      rewrite app_int_nil_r.
-      now rewrite <-DecimalZ.to_of, DecimalZ.of_to.
+  intro H.
+  apply (@f_equal _ _ (fun x => match x with Some x => x | _ => d end)
+                  (Some (dnorm d)) (Some (dnorm d'))).
+  now rewrite <- !to_of, H.
 Qed.
 
-Lemma of_decimal_dnormf d : of_decimal (dnormf d) = of_decimal d.
+Lemma of_iff d d' : of_decimal d = of_decimal d' <-> dnorm d = dnorm d'.
 Proof.
-  rewrite <-(of_decimal_dnorme d).
-  unfold of_decimal, dnormf.
-  assert (H : match dnorme d with Decimal _ f | DecimalExp _ f _ => f end = Nil).
-  { now unfold dnorme; destruct d;
-      (case norm; intro d; [case d; [|intro u; case u|..]|]). }
-  revert H; generalize (dnorme d); clear d; intro d.
-  destruct d; intro H; rewrite H; clear H; [now simpl|].
-  case (Z.of_int e); clear e; [|intro e..].
-  - now simpl.
-  - simpl.
-    rewrite app_int_nil_r.
-    apply f_equal2; [|reflexivity].
-    rewrite app_int_nil_r.
-    rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-    rewrite !Pos2Nat.inj_iter.
-    fold (Nat.iter (Pos.to_nat e) D0 Nil).
-    now rewrite of_int_iter_D0.
-  - simpl.
-    set (ai := match i with Pos _ => _ | _ => _ end).
-    rewrite app_int_nil_r.
-    case Nat.ltb_spec; intro Hei; simpl.
-    + rewrite nb_digits_del_head; [|now apply Nat.le_sub_l].
-      rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l].
-      rewrite Nat2Z.inj_sub; [|now apply le_Sn_le].
-      rewrite Z.sub_sub_distr, Z.sub_diag; simpl.
-      rewrite positive_nat_Z; simpl.
-      now revert Hei; unfold ai; case i; clear i ai; intros i Hei; simpl;
-        (rewrite app_del_tail_head; [|now apply le_Sn_le]).
-    + set (n := nb_digits _).
-      assert (H : (n = Pos.to_nat e - nb_digits ai + nb_digits ai)%nat).
-      { unfold n; induction (_ - _)%nat; [now simpl|].
-        now rewrite Unsigned.nat_iter_S; simpl; rewrite IHn0. }
-      rewrite H; clear n H.
-      rewrite Nat2Z.inj_add, (Nat2Z.inj_sub _ _ Hei).
-      rewrite <-Z.sub_sub_distr, Z.sub_diag, Z.sub_0_r.
-      rewrite positive_nat_Z; simpl.
-      rewrite <-(DecimalZ.of_to (Z.of_int (app_int _ _))), DecimalZ.to_of.
-      rewrite <-(DecimalZ.of_to (Z.of_int i)), DecimalZ.to_of.
-      apply f_equal2; [|reflexivity]; apply f_equal.
-      now unfold ai; case i; clear i ai Hei; intro i;
-        (induction (_ - _)%nat; [|rewrite <-IHn]).
+  split. apply of_inj. intros E. rewrite <- of_decimal_dnorm, E.
+  apply of_decimal_dnorm.
 Qed.
diff --git a/theories/Numbers/DecimalR.v b/theories/Numbers/DecimalR.v
new file mode 100644
index 0000000000..9b65a7dc20
--- /dev/null
+++ b/theories/Numbers/DecimalR.v
@@ -0,0 +1,312 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+(** * DecimalR
+
+    Proofs that conversions between decimal numbers and [R]
+    are bijections. *)
+
+Require Import Decimal DecimalFacts DecimalPos DecimalZ DecimalQ Rdefinitions.
+
+Lemma of_IQmake_to_decimal num den :
+  match IQmake_to_decimal num den with
+  | None => True
+  | Some (DecimalExp _ _ _) => False
+  | Some (Decimal i f) =>
+    of_decimal (Decimal i f) = IRQ (QArith_base.Qmake num den)
+  end.
+Proof.
+  unfold IQmake_to_decimal.
+  case (Pos.eq_dec den 1); [now intros->|intro Hden].
+  assert (Hf : match QArith_base.IQmake_to_decimal num den with
+               | Some (Decimal i f) => f <> Nil
+               | _ => True
+               end).
+  { unfold QArith_base.IQmake_to_decimal; simpl.
+    generalize (Unsigned.nztail_to_uint den).
+    case Decimal.nztail as [den' e_den'].
+    case den'; [now simpl|now simpl| |now simpl..]; clear den'; intro den'.
+    case den'; [ |now simpl..]; clear den'.
+    case e_den' as [|e_den']; [now simpl; intros H _; apply Hden; injection H|].
+    intros _.
+    case Nat.ltb_spec; intro He_den'.
+    - apply del_head_nonnil.
+      revert He_den'; case nb_digits as [|n]; [now simpl|].
+      now intro H; simpl; apply le_lt_n_Sm, Nat.le_sub_l.
+    - apply nb_digits_n0.
+      now rewrite nb_digits_iter_D0, Nat.sub_add. }
+  replace (match den with 1%positive => _ | _ => _ end)
+    with (QArith_base.IQmake_to_decimal num den); [|now revert Hden; case den].
+  generalize (of_IQmake_to_decimal num den).
+  case QArith_base.IQmake_to_decimal as [d'|]; [|now simpl].
+  case d' as [i f|]; [|now simpl].
+  unfold of_decimal; simpl.
+  intro H; injection H; clear H; intros <-.
+  intro H; generalize (f_equal QArith_base.IZ_to_Z H); clear H.
+  rewrite !IZ_to_Z_IZ_of_Z; intro H; injection H; clear H; intros<-.
+  now revert Hf; case f.
+Qed.
+
+Lemma of_to (q:IR) : forall d, to_decimal q = Some d -> of_decimal d = q.
+Proof.
+  intro d.
+  case q as [z|q|r r'|r r']; simpl.
+  - case z as [z p| |p|p].
+    + now simpl.
+    + now simpl; intro H; injection H; clear H; intros<-.
+    + simpl; intro H; injection H; clear H; intros<-.
+      now unfold of_decimal; simpl; unfold Z.of_uint; rewrite Unsigned.of_to.
+    + simpl; intro H; injection H; clear H; intros<-.
+      now unfold of_decimal; simpl; unfold Z.of_uint; rewrite Unsigned.of_to.
+  - case q as [num den].
+    generalize (of_IQmake_to_decimal num den).
+    case IQmake_to_decimal as [d'|]; [|now simpl].
+    case d' as [i f|]; [|now simpl].
+    now intros H H'; injection H'; intros<-.
+  - case r as [z|q| |]; [|case q as[num den]|now simpl..];
+      (case r' as [z'| | |]; [|now simpl..]);
+      (case z' as [p e| | |]; [|now simpl..]).
+    + case (Z.eq_dec p 10); [intros->|intro Hp].
+      2:{ revert Hp; case p; [now simpl|intro d0..];
+        (case d0; [intro d1..|]; [now simpl| |now simpl];
+         case d1; [intro d2..|]; [|now simpl..];
+         case d2; [intro d3..|]; [now simpl| |now simpl];
+         now case d3). }
+      case z as [| |p|p]; [now simpl|..]; intro H; injection H; intros<-.
+      * now unfold of_decimal; simpl; unfold Z.of_uint; rewrite Unsigned.of_to.
+      * unfold of_decimal; simpl; unfold Z.of_uint; rewrite Unsigned.of_to; simpl.
+        now rewrite Unsigned.of_to.
+      * unfold of_decimal; simpl; unfold Z.of_uint; rewrite Unsigned.of_to; simpl.
+        now rewrite Unsigned.of_to.
+    + case (Z.eq_dec p 10); [intros->|intro Hp].
+      2:{ revert Hp; case p; [now simpl|intro d0..];
+        (case d0; [intro d1..|]; [now simpl| |now simpl];
+         case d1; [intro d2..|]; [|now simpl..];
+         case d2; [intro d3..|]; [now simpl| |now simpl];
+         now case d3). }
+      generalize (of_IQmake_to_decimal num den).
+      case IQmake_to_decimal as [d'|]; [|now simpl].
+      case d' as [i f|]; [|now simpl].
+      intros H H'; injection H'; clear H'; intros<-.
+      unfold of_decimal; simpl.
+      change (match f with Nil => _ | _ => _ end) with (of_decimal (Decimal i f)).
+      rewrite H; clear H.
+      now unfold Z.of_uint; rewrite Unsigned.of_to.
+  - case r as [z|q| |]; [|case q as[num den]|now simpl..];
+      (case r' as [z'| | |]; [|now simpl..]);
+      (case z' as [p e| | |]; [|now simpl..]).
+    + case (Z.eq_dec p 10); [intros->|intro Hp].
+      2:{ revert Hp; case p; [now simpl|intro d0..];
+        (case d0; [intro d1..|]; [now simpl| |now simpl];
+         case d1; [intro d2..|]; [|now simpl..];
+         case d2; [intro d3..|]; [now simpl| |now simpl];
+         now case d3). }
+      case z as [| |p|p]; [now simpl|..]; intro H; injection H; intros<-.
+      * now unfold of_decimal; simpl; unfold Z.of_uint; rewrite Unsigned.of_to.
+      * unfold of_decimal; simpl; unfold Z.of_uint; rewrite Unsigned.of_to; simpl.
+        now rewrite Unsigned.of_to.
+      * unfold of_decimal; simpl; unfold Z.of_uint; rewrite Unsigned.of_to; simpl.
+        now rewrite Unsigned.of_to.
+    + case (Z.eq_dec p 10); [intros->|intro Hp].
+      2:{ revert Hp; case p; [now simpl|intro d0..];
+        (case d0; [intro d1..|]; [now simpl| |now simpl];
+         case d1; [intro d2..|]; [|now simpl..];
+         case d2; [intro d3..|]; [now simpl| |now simpl];
+         now case d3). }
+      generalize (of_IQmake_to_decimal num den).
+      case IQmake_to_decimal as [d'|]; [|now simpl].
+      case d' as [i f|]; [|now simpl].
+      intros H H'; injection H'; clear H'; intros<-.
+      unfold of_decimal; simpl.
+      change (match f with Nil => _ | _ => _ end) with (of_decimal (Decimal i f)).
+      rewrite H; clear H.
+      now unfold Z.of_uint; rewrite Unsigned.of_to.
+Qed.
+
+Lemma to_of (d:decimal) : to_decimal (of_decimal d) = Some (dnorm d).
+Proof.
+  case d as [i f|i f e].
+  - unfold of_decimal; simpl.
+    case (uint_eq_dec f Nil); intro Hf.
+    + rewrite Hf; clear f Hf.
+      unfold to_decimal; simpl.
+      rewrite IZ_to_Z_IZ_of_Z, DecimalZ.to_of.
+      case i as [i|i]; [now simpl|]; simpl.
+      rewrite app_nil_r.
+      case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi].
+      now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead.
+    + set (r := IRQ _).
+      set (m := match f with Nil => _ | _ => _ end).
+      replace m with r; [unfold r|now unfold m; revert Hf; case f].
+      unfold to_decimal; simpl.
+      unfold IQmake_to_decimal; simpl.
+      set (n := Nat.iter _ _ _).
+      case (Pos.eq_dec n 1); intro Hn.
+      exfalso; apply Hf.
+      { now apply nb_digits_0; revert Hn; unfold n; case nb_digits. }
+      clear m; set (m := match n with 1%positive | _ => _ end).
+      replace m with (QArith_base.IQmake_to_decimal (Z.of_int (app_int i f)) n).
+      2:{ now unfold m; revert Hn; case n. }
+      unfold QArith_base.IQmake_to_decimal, n; simpl.
+      rewrite nztail_to_uint_pow10.
+      clear r; set (r := if _ <? _ then Some (Decimal _ _) else Some _).
+      clear m; set (m := match nb_digits f with 0 => _ | _ => _ end).
+      replace m with r; [unfold r|now unfold m; revert Hf; case f].
+      rewrite DecimalZ.to_of, abs_norm, abs_app_int.
+      case Nat.ltb_spec; intro Hnf.
+      * rewrite (del_tail_app_int_exact _ _ Hnf).
+        rewrite (del_head_app_int_exact _ _ Hnf).
+        now rewrite (dnorm_i_exact _ _ Hnf).
+      * rewrite (unorm_app_r _ _ Hnf).
+        rewrite (iter_D0_unorm _ Hf).
+        now rewrite dnorm_i_exact'.
+  - unfold of_decimal; simpl.
+    rewrite <-(DecimalZ.to_of e).
+    case (Z.of_int e); clear e; [|intro e..]; simpl.
+    + case (uint_eq_dec f Nil); intro Hf.
+      * rewrite Hf; clear f Hf.
+        unfold to_decimal; simpl.
+        rewrite IZ_to_Z_IZ_of_Z, DecimalZ.to_of.
+        case i as [i|i]; [now simpl|]; simpl.
+        rewrite app_nil_r.
+        case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi].
+        now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead.
+      * set (r := IRQ _).
+        set (m := match f with Nil => _ | _ => _ end).
+        replace m with r; [unfold r|now unfold m; revert Hf; case f].
+        unfold to_decimal; simpl.
+        unfold IQmake_to_decimal; simpl.
+        set (n := Nat.iter _ _ _).
+        case (Pos.eq_dec n 1); intro Hn.
+        exfalso; apply Hf.
+        { now apply nb_digits_0; revert Hn; unfold n; case nb_digits. }
+        clear m; set (m := match n with 1%positive | _ => _ end).
+        replace m with (QArith_base.IQmake_to_decimal (Z.of_int (app_int i f)) n).
+        2:{ now unfold m; revert Hn; case n. }
+        unfold QArith_base.IQmake_to_decimal, n; simpl.
+        rewrite nztail_to_uint_pow10.
+        clear r; set (r := if _ <? _ then Some (Decimal _ _) else Some _).
+        clear m; set (m := match nb_digits f with 0 => _ | _ => _ end).
+        replace m with r; [unfold r|now unfold m; revert Hf; case f].
+        rewrite DecimalZ.to_of, abs_norm, abs_app_int.
+        case Nat.ltb_spec; intro Hnf.
+        -- rewrite (del_tail_app_int_exact _ _ Hnf).
+           rewrite (del_head_app_int_exact _ _ Hnf).
+           now rewrite (dnorm_i_exact _ _ Hnf).
+        -- rewrite (unorm_app_r _ _ Hnf).
+           rewrite (iter_D0_unorm _ Hf).
+           now rewrite dnorm_i_exact'.
+    + set (i' := match i with Pos _ => _ | _ => _ end).
+      set (m := match Pos.to_uint e with Nil => _ | _ => _ end).
+      replace m with (DecimalExp i' f (Pos (Pos.to_uint e))).
+      2:{ unfold m; generalize (Unsigned.to_uint_nonzero e).
+          now case Pos.to_uint; [|intro u; case u|..]. }
+      unfold i'; clear i' m.
+      case (uint_eq_dec f Nil); intro Hf.
+      * rewrite Hf; clear f Hf.
+        unfold to_decimal; simpl.
+        rewrite IZ_to_Z_IZ_of_Z, DecimalZ.to_of.
+        case i as [i|i]; [now simpl|]; simpl.
+        rewrite app_nil_r.
+        case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi].
+        now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead.
+      * set (r := IRQ _).
+        set (m := match f with Nil => _ | _ => _ end).
+        replace m with r; [unfold r|now unfold m; revert Hf; case f].
+        unfold to_decimal; simpl.
+        unfold IQmake_to_decimal; simpl.
+        set (n := Nat.iter _ _ _).
+        case (Pos.eq_dec n 1); intro Hn.
+        exfalso; apply Hf.
+        { now apply nb_digits_0; revert Hn; unfold n; case nb_digits. }
+        clear m; set (m := match n with 1%positive | _ => _ end).
+        replace m with (QArith_base.IQmake_to_decimal (Z.of_int (app_int i f)) n).
+        2:{ now unfold m; revert Hn; case n. }
+        unfold QArith_base.IQmake_to_decimal, n; simpl.
+        rewrite nztail_to_uint_pow10.
+        clear r; set (r := if _ <? _ then Some (Decimal _ _) else Some _).
+        clear m; set (m := match nb_digits f with 0 => _ | _ => _ end).
+        replace m with r; [unfold r|now unfold m; revert Hf; case f].
+        rewrite DecimalZ.to_of, abs_norm, abs_app_int.
+        case Nat.ltb_spec; intro Hnf.
+        -- rewrite (del_tail_app_int_exact _ _ Hnf).
+           rewrite (del_head_app_int_exact _ _ Hnf).
+           now rewrite (dnorm_i_exact _ _ Hnf).
+        -- rewrite (unorm_app_r _ _ Hnf).
+           rewrite (iter_D0_unorm _ Hf).
+           now rewrite dnorm_i_exact'.
+    + case (uint_eq_dec f Nil); intro Hf.
+      * rewrite Hf; clear f Hf.
+        unfold to_decimal; simpl.
+        rewrite IZ_to_Z_IZ_of_Z, DecimalZ.to_of.
+        case i as [i|i]; [now simpl|]; simpl.
+        rewrite app_nil_r.
+        case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi].
+        now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead.
+      * set (r := IRQ _).
+        set (m := match f with Nil => _ | _ => _ end).
+        replace m with r; [unfold r|now unfold m; revert Hf; case f].
+        unfold to_decimal; simpl.
+        unfold IQmake_to_decimal; simpl.
+        set (n := Nat.iter _ _ _).
+        case (Pos.eq_dec n 1); intro Hn.
+        exfalso; apply Hf.
+        { now apply nb_digits_0; revert Hn; unfold n; case nb_digits. }
+        clear m; set (m := match n with 1%positive | _ => _ end).
+        replace m with (QArith_base.IQmake_to_decimal (Z.of_int (app_int i f)) n).
+        2:{ now unfold m; revert Hn; case n. }
+        unfold QArith_base.IQmake_to_decimal, n; simpl.
+        rewrite nztail_to_uint_pow10.
+        clear r; set (r := if _ <? _ then Some (Decimal _ _) else Some _).
+        clear m; set (m := match nb_digits f with 0 => _ | _ => _ end).
+        replace m with r; [unfold r|now unfold m; revert Hf; case f].
+        rewrite DecimalZ.to_of, abs_norm, abs_app_int.
+        case Nat.ltb_spec; intro Hnf.
+        -- rewrite (del_tail_app_int_exact _ _ Hnf).
+           rewrite (del_head_app_int_exact _ _ Hnf).
+           now rewrite (dnorm_i_exact _ _ Hnf).
+        -- rewrite (unorm_app_r _ _ Hnf).
+           rewrite (iter_D0_unorm _ Hf).
+           now rewrite dnorm_i_exact'.
+Qed.
+
+(** Some consequences *)
+
+Lemma to_decimal_inj q q' :
+  to_decimal q <> None -> to_decimal q = to_decimal q' -> q = q'.
+Proof.
+  intros Hnone EQ.
+  generalize (of_to q) (of_to q').
+  rewrite <-EQ.
+  revert Hnone; case to_decimal; [|now simpl].
+  now intros d _ H1 H2; rewrite <-(H1 d eq_refl), <-(H2 d eq_refl).
+Qed.
+
+Lemma to_decimal_surj d : exists q, to_decimal q = Some (dnorm d).
+Proof.
+  exists (of_decimal d). apply to_of.
+Qed.
+
+Lemma of_decimal_dnorm d : of_decimal (dnorm d) = of_decimal d.
+Proof. now apply to_decimal_inj; rewrite !to_of; [|rewrite dnorm_involutive]. Qed.
+
+Lemma of_inj d d' : of_decimal d = of_decimal d' -> dnorm d = dnorm d'.
+Proof.
+  intro H.
+  apply (@f_equal _ _ (fun x => match x with Some x => x | _ => d end)
+                  (Some (dnorm d)) (Some (dnorm d'))).
+  now rewrite <- !to_of, H.
+Qed.
+
+Lemma of_iff d d' : of_decimal d = of_decimal d' <-> dnorm d = dnorm d'.
+Proof.
+  split. apply of_inj. intros E. rewrite <- of_decimal_dnorm, E.
+  apply of_decimal_dnorm.
+Qed.
diff --git a/theories/Numbers/DecimalZ.v b/theories/Numbers/DecimalZ.v
index 69d8073fc7..faaf8a3932 100644
--- a/theories/Numbers/DecimalZ.v
+++ b/theories/Numbers/DecimalZ.v
@@ -79,9 +79,11 @@ Qed.
 Lemma of_uint_iter_D0 d n :
   Z.of_uint (app d (Nat.iter n D0 Nil)) = Nat.iter n (Z.mul 10) (Z.of_uint d).
 Proof.
-  unfold Z.of_uint.
-  unfold app; rewrite <-rev_revapp.
-  rewrite Unsigned.of_lu_rev, Unsigned.of_lu_revapp.
+  rewrite <-(rev_rev (app _ _)), <-(of_list_to_list (rev (app _ _))).
+  rewrite rev_spec, app_spec, List.rev_app_distr.
+  rewrite <-!rev_spec, <-app_spec, of_list_to_list.
+  unfold Z.of_uint; rewrite Unsigned.of_lu_rev.
+  unfold app; rewrite Unsigned.of_lu_revapp, !rev_rev.
   rewrite <-!Unsigned.of_lu_rev, !rev_rev.
   assert (H' : Pos.of_uint (Nat.iter n D0 Nil) = 0%N).
   { now induction n; [|rewrite Unsigned.nat_iter_S]. }
@@ -100,3 +102,22 @@ Proof.
   - rewrite of_uint_iter_D0; induction n; [now simpl|].
     rewrite !Unsigned.nat_iter_S, <-IHn; ring.
 Qed.
+
+Lemma nztail_to_uint_pow10 n :
+  Decimal.nztail (Pos.to_uint (Nat.iter n (Pos.mul 10) 1%positive))
+  = (D1 Nil, n).
+Proof.
+  case n as [|n]; [now simpl|].
+  rewrite <-(Nat2Pos.id (S n)); [|now simpl].
+  generalize (Pos.of_nat (S n)); clear n; intro p.
+  induction (Pos.to_nat p); [now simpl|].
+  rewrite Unsigned.nat_iter_S.
+  unfold Pos.to_uint.
+  change (Pos.to_little_uint _)
+    with (Unsigned.to_lu (10 * N.pos (Nat.iter n (Pos.mul 10) 1%positive))).
+  rewrite Unsigned.to_ldec_tenfold.
+  revert IHn; unfold Pos.to_uint.
+  unfold Decimal.nztail; rewrite !rev_rev; simpl.
+  set (f'' := _ (Pos.to_little_uint _)).
+  now case f''; intros r n' H; inversion H.
+Qed.
diff --git a/theories/Numbers/HexadecimalFacts.v b/theories/Numbers/HexadecimalFacts.v
index 7328b2303d..c624b4e6b9 100644
--- a/theories/Numbers/HexadecimalFacts.v
+++ b/theories/Numbers/HexadecimalFacts.v
@@ -10,136 +10,437 @@
 
 (** * HexadecimalFacts : some facts about Hexadecimal numbers *)
 
-Require Import Hexadecimal Arith.
+Require Import Hexadecimal Arith ZArith.
+
+Variant digits :=
+  | d0 | d1 | d2 | d3 | d4 | d5 | d6 | d7 | d8 | d9
+  | da | db | dc | dd | de | df.
+
+Fixpoint to_list (u : uint) : list digits :=
+  match u with
+  | Nil => nil
+  | D0 u => cons d0 (to_list u)
+  | D1 u => cons d1 (to_list u)
+  | D2 u => cons d2 (to_list u)
+  | D3 u => cons d3 (to_list u)
+  | D4 u => cons d4 (to_list u)
+  | D5 u => cons d5 (to_list u)
+  | D6 u => cons d6 (to_list u)
+  | D7 u => cons d7 (to_list u)
+  | D8 u => cons d8 (to_list u)
+  | D9 u => cons d9 (to_list u)
+  | Da u => cons da (to_list u)
+  | Db u => cons db (to_list u)
+  | Dc u => cons dc (to_list u)
+  | Dd u => cons dd (to_list u)
+  | De u => cons de (to_list u)
+  | Df u => cons df (to_list u)
+  end.
+
+Fixpoint of_list (l : list digits) : uint :=
+  match l with
+  | nil => Nil
+  | cons d0 l => D0 (of_list l)
+  | cons d1 l => D1 (of_list l)
+  | cons d2 l => D2 (of_list l)
+  | cons d3 l => D3 (of_list l)
+  | cons d4 l => D4 (of_list l)
+  | cons d5 l => D5 (of_list l)
+  | cons d6 l => D6 (of_list l)
+  | cons d7 l => D7 (of_list l)
+  | cons d8 l => D8 (of_list l)
+  | cons d9 l => D9 (of_list l)
+  | cons da l => Da (of_list l)
+  | cons db l => Db (of_list l)
+  | cons dc l => Dc (of_list l)
+  | cons dd l => Dd (of_list l)
+  | cons de l => De (of_list l)
+  | cons df l => Df (of_list l)
+  end.
 
-Scheme Equality for uint.
+Lemma of_list_to_list u : of_list (to_list u) = u.
+Proof. now induction u; [|simpl; rewrite IHu..]. Qed.
 
-Scheme Equality for int.
+Lemma to_list_of_list l : to_list (of_list l) = l.
+Proof. now induction l as [|h t IHl]; [|case h; simpl; rewrite IHl]. Qed.
 
-Lemma rev_revapp d d' :
-  rev (revapp d d') = revapp d' d.
+Lemma to_list_inj u u' : to_list u = to_list u' -> u = u'.
 Proof.
-  revert d'. induction d; simpl; intros; now rewrite ?IHd.
+  now intro H; rewrite <-(of_list_to_list u), <-(of_list_to_list u'), H.
 Qed.
 
-Lemma rev_rev d : rev (rev d) = d.
+Lemma of_list_inj u u' : of_list u = of_list u' -> u = u'.
 Proof.
-  apply rev_revapp.
+  now intro H; rewrite <-(to_list_of_list u), <-(to_list_of_list u'), H.
 Qed.
 
-Lemma revapp_rev_nil d : revapp (rev d) Nil = d.
-Proof. now fold (rev (rev d)); rewrite rev_rev. Qed.
+Lemma nb_digits_spec u : nb_digits u = length (to_list u).
+Proof. now induction u; [|simpl; rewrite IHu..]. Qed.
 
-Lemma app_nil_r d : app d Nil = d.
-Proof. now unfold app; rewrite revapp_rev_nil. Qed.
+Fixpoint lnzhead l :=
+  match l with
+  | nil => nil
+  | cons d l' =>
+    match d with
+    | d0 => lnzhead l'
+    | _ => l
+    end
+  end.
 
-Lemma app_int_nil_r d : app_int d Nil = d.
-Proof. now case d; intro d'; simpl; rewrite app_nil_r. Qed.
+Lemma nzhead_spec u : to_list (nzhead u) = lnzhead (to_list u).
+Proof. now induction u; [|simpl; rewrite IHu|..]. Qed.
+
+Definition lzero := cons d0 nil.
+
+Definition lunorm l :=
+  match lnzhead l with
+  | nil => lzero
+  | d => d
+  end.
+
+Lemma unorm_spec u : to_list (unorm u) = lunorm (to_list u).
+Proof. now unfold unorm, lunorm; rewrite <-nzhead_spec; case (nzhead u). Qed.
+
+Lemma revapp_spec d d' :
+  to_list (revapp d d') = List.rev_append (to_list d) (to_list d').
+Proof. now revert d'; induction d; intro d'; [|simpl; rewrite IHd..]. Qed.
+
+Lemma rev_spec d : to_list (rev d) = List.rev (to_list d).
+Proof. now unfold rev; rewrite revapp_spec, List.rev_alt; simpl. Qed.
+
+Lemma app_spec d d' :
+  to_list (app d d') = Datatypes.app (to_list d) (to_list d').
+Proof.
+  unfold app.
+  now rewrite revapp_spec, List.rev_append_rev, rev_spec, List.rev_involutive.
+Qed.
 
-Lemma revapp_revapp_1 d d' d'' :
-  nb_digits d <= 1 ->
-  revapp (revapp d d') d'' = revapp d' (revapp d d'').
+Definition lnztail l :=
+  let fix aux l_rev :=
+    match l_rev with
+    | cons d0 l_rev => let (r, n) := aux l_rev in pair r (S n)
+    | _ => pair l_rev O
+    end in
+  let (r, n) := aux (List.rev l) in pair (List.rev r) n.
+
+Lemma nztail_spec d :
+  let (r, n) := nztail d in
+  let (r', n') := lnztail (to_list d) in
+  to_list r = r' /\ n = n'.
 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))]..]..].
+  unfold nztail, lnztail.
+  set (f := fix aux d_rev := match d_rev with
+            | D0 d_rev => let (r, n) := aux d_rev in (r, S n)
+            | _ => (d_rev, 0) end).
+  set (f' := fix aux (l_rev : list digits) : list digits * nat :=
+             match l_rev with
+             | cons d0 l_rev => let (r, n) := aux l_rev in (r, S n)
+             | _ => (l_rev, 0)
+             end).
+  rewrite <-(of_list_to_list (rev d)), rev_spec.
+  induction (List.rev _) as [|h t IHl]; [now simpl|].
+  case h; simpl; [|now rewrite rev_spec; simpl; rewrite to_list_of_list..].
+  now revert IHl; case f; intros r n; case f'; intros r' n' [-> ->].
 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 del_head_spec_0 d : del_head 0 d = d.
+Proof. now simpl. Qed.
 
-Lemma nb_digits_revapp d d' :
-  nb_digits (revapp d d') = nb_digits d + nb_digits d'.
+Lemma del_head_spec_small n d :
+  n <= length (to_list d) -> to_list (del_head n d) = List.skipn n (to_list d).
 Proof.
-  now revert d'; induction d; [|intro d'; simpl; rewrite IHd; simpl..].
+  revert d; induction n as [|n IHn]; intro d; [now simpl|].
+  now case d; [|intros d' H; apply IHn, le_S_n..].
 Qed.
 
-Lemma nb_digits_rev u : nb_digits (rev u) = nb_digits u.
-Proof. now unfold rev; rewrite nb_digits_revapp. Qed.
+Lemma del_head_spec_large n d : length (to_list d) < n -> del_head n d = zero.
+Proof.
+  revert d; induction n; intro d; [now case d|].
+  now case d; [|intro d'; simpl; intro H; rewrite (IHn _ (lt_S_n _ _ H))..].
+Qed.
 
-Lemma nb_digits_nzhead u : nb_digits (nzhead u) <= nb_digits u.
-Proof. now induction u; [|apply le_S|..]. Qed.
+Lemma nb_digits_0 d : nb_digits d = 0 -> d = Nil.
+Proof.
+  rewrite nb_digits_spec, <-(of_list_to_list d).
+  now case (to_list d) as [|h t]; [|rewrite to_list_of_list].
+Qed.
+
+Lemma nb_digits_n0 d : nb_digits d <> 0 -> d <> Nil.
+Proof. now case d; [|intros u _..]. 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 length_lnzhead l : length (lnzhead l) <= length l.
+Proof. now induction l as [|h t IHl]; [|case h; [apply le_S|..]]. Qed.
+
+Lemma nb_digits_nzhead u : nb_digits (nzhead u) <= nb_digits u.
+Proof. now induction u; [|apply le_S|..]. Qed.
 
-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|]|]]..].
+Lemma unorm_nzhead u : nzhead u <> Nil -> unorm u = nzhead u.
+Proof. now unfold unorm; case nzhead. Qed.
+
+Lemma nb_digits_unorm u : u <> Nil -> nb_digits (unorm u) <= nb_digits u.
+Proof.
+  intro Hu; case (uint_eq_dec (nzhead u) Nil).
+  { unfold unorm; intros ->; simpl.
+    now revert Hu; case u; [|intros u' _; apply le_n_S, Nat.le_0_l..]. }
+  intro H; rewrite (unorm_nzhead _ H); apply nb_digits_nzhead.
+Qed.
+
+Lemma nb_digits_rev d : nb_digits (rev d) = nb_digits d.
+Proof. now rewrite !nb_digits_spec, rev_spec, List.rev_length. Qed.
+
+Lemma nb_digits_del_head_sub d n :
+  n <= nb_digits d ->
+  nb_digits (del_head (nb_digits d - n) d) = n.
+Proof.
+  rewrite !nb_digits_spec; intro Hn.
+  rewrite del_head_spec_small; [|now apply Nat.le_sub_l].
+  rewrite List.skipn_length, <-(Nat2Z.id (_ - _)).
+  rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l].
+  rewrite (Nat2Z.inj_sub _ _ Hn).
+  rewrite Z.sub_sub_distr, Z.sub_diag; apply Nat2Z.id.
+Qed.
+
+Lemma unorm_D0 u : unorm (D0 u) = unorm u.
+Proof. reflexivity. Qed.
+
+Lemma app_nil_l d : app Nil d = d.
+Proof. now simpl. Qed.
+
+Lemma app_nil_r d : app d Nil = d.
+Proof. now apply to_list_inj; rewrite app_spec, List.app_nil_r. Qed.
+
+Lemma abs_app_int d d' : abs (app_int d d') = app (abs d) d'.
+Proof. now case d. Qed.
+
+Lemma abs_norm d : abs (norm d) = unorm (abs d).
+Proof. now case d as [u|u]; [|simpl; unfold unorm; case nzhead]. Qed.
+
+Lemma iter_D0_nzhead d :
+  Nat.iter (nb_digits d - nb_digits (nzhead d)) D0 (nzhead d) = d.
+Proof.
+  induction d; [now simpl| |now rewrite Nat.sub_diag..].
+  simpl nzhead; simpl nb_digits.
+  rewrite (Nat.sub_succ_l _ _ (nb_digits_nzhead _)).
+  now rewrite <-IHd at 4.
+Qed.
+
+Lemma iter_D0_unorm d :
+  d <> Nil ->
+  Nat.iter (nb_digits d - nb_digits (unorm d)) D0 (unorm d) = d.
+Proof.
+  case (uint_eq_dec (nzhead d) Nil); intro Hn.
+  { unfold unorm; rewrite Hn; simpl; intro H.
+    revert H Hn; induction d; [now simpl|intros _|now intros _..].
+    case (uint_eq_dec d Nil); simpl; intros H Hn; [now rewrite H|].
+    rewrite Nat.sub_0_r, (le_plus_minus 1 (nb_digits d)).
+    { now simpl; rewrite IHd. }
+    revert H; case d; [now simpl|intros u _; apply le_n_S, Nat.le_0_l..]. }
+  intros _; rewrite (unorm_nzhead _ Hn); apply iter_D0_nzhead.
+Qed.
+
+Lemma nzhead_app_l d d' :
+  nb_digits d' < nb_digits (nzhead (app d d')) ->
+  nzhead (app d d') = app (nzhead d) d'.
+Proof.
+  intro Hl; apply to_list_inj; revert Hl.
+  rewrite !nb_digits_spec, app_spec, !nzhead_spec, app_spec.
+  induction (to_list d) as [|h t IHl].
+  { now simpl; intro H; exfalso; revert H; apply le_not_lt, length_lnzhead. }
+  rewrite <-List.app_comm_cons.
+  now case h; [simpl; intro Hl; apply IHl|..].
+Qed.
+
+Lemma nzhead_app_r d d' :
+  nb_digits (nzhead (app d d')) <= nb_digits d' ->
+  nzhead (app d d') = nzhead d'.
+Proof.
+  intro Hl; apply to_list_inj; revert Hl.
+  rewrite !nb_digits_spec, !nzhead_spec, app_spec.
+  induction (to_list d) as [|h t IHl]; [now simpl|].
+  rewrite <-List.app_comm_cons.
+  now case h; [| simpl; rewrite List.app_length; intro Hl; exfalso; revert Hl;
+    apply le_not_lt, le_plus_r..].
+Qed.
+
+Lemma nzhead_app_nil_r d d' : nzhead (app d d') = Nil -> nzhead d' = Nil.
+Proof.
+now intro H; generalize H; rewrite nzhead_app_r; [|rewrite H; apply Nat.le_0_l].
+Qed.
+
+Lemma nzhead_app_nil d d' :
+  nb_digits (nzhead (app d d')) <= nb_digits d' -> nzhead d = Nil.
+Proof.
+  intro H; apply to_list_inj; revert H.
+  rewrite !nb_digits_spec, !nzhead_spec, app_spec.
+  induction (to_list d) as [|h t IHl]; [now simpl|].
+  now case h; [now simpl|..];
+    simpl;intro H; exfalso; revert H; apply le_not_lt;
+    rewrite List.app_length; apply le_plus_r.
+Qed.
+
+Lemma nzhead_app_nil_l d d' : nzhead (app d d') = Nil -> nzhead d = Nil.
+Proof.
+  intro H; apply to_list_inj; generalize (f_equal to_list H); clear H.
+  rewrite !nzhead_spec, app_spec.
+  induction (to_list d) as [|h t IHl]; [now simpl|].
+  now rewrite <-List.app_comm_cons; case h.
+Qed.
+
+Lemma unorm_app_zero d d' :
+  nb_digits (unorm (app d d')) <= nb_digits d' -> unorm d = zero.
+Proof.
+  unfold unorm.
+  case (uint_eq_dec (nzhead (app d d')) Nil).
+  { now intro Hn; rewrite Hn, (nzhead_app_nil_l _ _ Hn). }
+  intro H; fold (unorm (app d d')); rewrite (unorm_nzhead _ H); intro H'.
+  case (uint_eq_dec (nzhead d) Nil); [now intros->|].
+  intro H''; fold (unorm d); rewrite (unorm_nzhead _ H'').
+  exfalso; apply H''; revert H'; apply nzhead_app_nil.
+Qed.
+
+Lemma app_int_nil_r d : app_int d Nil = d.
+Proof.
+  now case d; intro d'; simpl;
+    rewrite <-(of_list_to_list (app _ _)), app_spec;
+    rewrite List.app_nil_r, of_list_to_list.
+Qed.
+
+Lemma unorm_app_l d d' :
+  nb_digits d' < nb_digits (unorm (app d d')) ->
+  unorm (app d d') = app (unorm d) d'.
+Proof.
+  case (uint_eq_dec d' Nil); [now intros->; rewrite !app_nil_r|intro Hd'].
+  case (uint_eq_dec (nzhead (app d d')) Nil).
+  { unfold unorm; intros->; simpl; intro H; exfalso; revert H; apply le_not_lt.
+    now revert Hd'; case d'; [|intros d'' _; apply le_n_S, Peano.le_0_n..]. }
+  intro Ha; rewrite (unorm_nzhead _ Ha).
+  intro Hn; generalize Hn; rewrite (nzhead_app_l _ _ Hn).
+  rewrite !nb_digits_spec, app_spec, List.app_length.
+  case (uint_eq_dec (nzhead d) Nil).
+  { intros->; simpl; intro H; exfalso; revert H; apply Nat.lt_irrefl. }
+  now intro H; rewrite (unorm_nzhead _ H).
+Qed.
+
+Lemma unorm_app_r d d' :
+  nb_digits (unorm (app d d')) <= nb_digits d' ->
+  unorm (app d d') = unorm d'.
+Proof.
+  case (uint_eq_dec (nzhead (app d d')) Nil).
+  { now unfold unorm; intro H; rewrite H, (nzhead_app_nil_r _ _ H). }
+  intro Ha; rewrite (unorm_nzhead _ Ha).
+  case (uint_eq_dec (nzhead d') Nil).
+  { now intros H H'; exfalso; apply Ha; rewrite nzhead_app_r. }
+  intro Hd'; rewrite (unorm_nzhead _ Hd'); apply nzhead_app_r.
+Qed.
+
+Lemma norm_app_int d d' :
+  nb_digits d' < nb_digits (unorm (app (abs d) d')) ->
+  norm (app_int d d') = app_int (norm d) d'.
+Proof.
+  case (uint_eq_dec d' Nil); [now intros->; rewrite !app_int_nil_r|intro Hd'].
+  case d as [d|d]; [now simpl; intro H; apply f_equal, unorm_app_l|].
+  simpl; unfold unorm.
+  case (uint_eq_dec (nzhead (app d d')) Nil).
+  { intros->; simpl; intro H; exfalso; revert H; apply le_not_lt.
+    now revert Hd'; case d'; [|intros d'' _; apply le_n_S, Peano.le_0_n..]. }
+  set (m := match nzhead _ with Nil => _ | _ => _ end).
+  intro Ha.
+  replace m with (nzhead (app d d')).
+  2:{ now unfold m; revert Ha; case nzhead. }
+  intro Hn; generalize Hn; rewrite (nzhead_app_l _ _ Hn).
+  case (uint_eq_dec (app (nzhead d) d') Nil).
+  { intros->; simpl; intro H; exfalso; revert H; apply le_not_lt, Nat.le_0_l. }
+  clear m; set (m := match app _ _ with Nil => _ | _ => _ end).
+  intro Ha'.
+  replace m with (Neg (app (nzhead d) d')); [|now unfold m; revert Ha'; case app].
+  case (uint_eq_dec (nzhead d) Nil).
+  { intros->; simpl; intro H; exfalso; revert H; apply Nat.lt_irrefl. }
+  clear m; set (m := match nzhead _ with Nil => _ | _ => _ end).
+  intro Hd.
+  now replace m with (Neg (nzhead d)); [|unfold m; revert Hd; case nzhead].
+Qed.
+
+Lemma del_head_nb_digits d : del_head (nb_digits d) d = Nil.
+Proof.
+  apply to_list_inj.
+  rewrite nb_digits_spec, del_head_spec_small; [|now simpl].
+  now rewrite List.skipn_all.
+Qed.
+
+Lemma del_tail_nb_digits d : del_tail (nb_digits d) d = Nil.
+Proof. now unfold del_tail; rewrite <-nb_digits_rev, del_head_nb_digits. Qed.
+
+Lemma del_head_app n d d' :
+  n <= nb_digits d -> del_head n (app d d') = app (del_head n d) d'.
+Proof.
+  rewrite nb_digits_spec; intro Hn.
+  apply to_list_inj.
+  rewrite del_head_spec_small.
+  2:{ now rewrite app_spec, List.app_length; apply le_plus_trans. }
+  rewrite !app_spec, (del_head_spec_small _ _ Hn).
+  rewrite List.skipn_app.
+  now rewrite (proj2 (Nat.sub_0_le _ _) Hn).
+Qed.
+
+Lemma del_tail_app n d d' :
+  n <= nb_digits d' -> del_tail n (app d d') = app d (del_tail n d').
+Proof.
+  rewrite nb_digits_spec; intro Hn.
+  unfold del_tail.
+  rewrite <-(of_list_to_list (rev (app d d'))), rev_spec, app_spec.
+  rewrite List.rev_app_distr, <-!rev_spec, <-app_spec, of_list_to_list.
+  rewrite del_head_app; [|now rewrite nb_digits_spec, rev_spec, List.rev_length].
+  apply to_list_inj.
+  rewrite rev_spec, !app_spec, !rev_spec.
+  now rewrite List.rev_app_distr, List.rev_involutive.
+Qed.
+
+Lemma del_tail_app_int n d d' :
+  n <= nb_digits d' -> del_tail_int n (app_int d d') = app_int d (del_tail n d').
+Proof. now case d as [d|d]; simpl; intro H; rewrite del_tail_app. Qed.
+
+Lemma app_del_tail_head n (d:uint) :
+  n <= nb_digits d -> app (del_tail n d) (del_head (nb_digits d - n) d) = d.
+Proof.
+  rewrite nb_digits_spec; intro Hn; unfold del_tail.
+  rewrite <-(of_list_to_list (app _ _)), app_spec, rev_spec.
+  rewrite del_head_spec_small; [|now rewrite rev_spec, List.rev_length].
+  rewrite del_head_spec_small; [|now apply Nat.le_sub_l].
+  rewrite rev_spec.
+  set (n' := _ - n).
+  assert (Hn' : n = length (to_list d) - n').
+  { now apply plus_minus; rewrite  Nat.add_comm; symmetry; apply le_plus_minus_r. }
+  now rewrite Hn', <-List.firstn_skipn_rev, List.firstn_skipn, of_list_to_list.
+Qed.
+
+Lemma app_int_del_tail_head n (d:int) :
+  n <= nb_digits (abs d) ->
+  app_int (del_tail_int n d) (del_head (nb_digits (abs d) - n) (abs d)) = d.
+Proof. now case d; clear d; simpl; intros u Hu; rewrite app_del_tail_head. Qed.
+
+Lemma del_head_app_int_exact i f :
+  nb_digits f < nb_digits (unorm (app (abs i) f)) ->
+  del_head (nb_digits (unorm (app (abs i) f)) - nb_digits f) (unorm (app (abs i) f)) = f.
+Proof.
+  simpl; intro Hnb; generalize Hnb; rewrite (unorm_app_l _ _ Hnb); clear Hnb.
+  replace (_ - _) with (nb_digits (unorm (abs i))).
+  - now rewrite del_head_app; [rewrite del_head_nb_digits|].
+  - rewrite !nb_digits_spec, app_spec, List.app_length.
+    now rewrite Nat.add_comm, minus_plus.
+Qed.
+
+Lemma del_tail_app_int_exact i f :
+  nb_digits f < nb_digits (unorm (app (abs i) f)) ->
+  del_tail_int (nb_digits f) (norm (app_int i f)) = norm i.
+Proof.
+  simpl; intro Hnb.
+  rewrite (norm_app_int _ _ Hnb).
+  rewrite del_tail_app_int; [|now simpl].
+  now rewrite del_tail_nb_digits, app_int_nil_r.
 Qed.
 
 (** Normalization on little-endian numbers *)
@@ -193,6 +494,9 @@ Proof.
   apply nzhead_revapp.
 Qed.
 
+Lemma rev_rev d : rev (rev d) = d.
+Proof. now apply to_list_inj; rewrite !rev_spec, List.rev_involutive. Qed.
+
 Lemma rev_nztail_rev d :
   rev (nztail (rev d)) = nzhead d.
 Proof.
@@ -247,47 +551,128 @@ 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.
+Lemma del_head_nonnil n u :
+  n < nb_digits u -> del_head n u <> Nil.
 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.
+  now revert n; induction u; intro n;
+    [|case n; [|intro n'; simpl; intro H; apply IHu, lt_S_n]..].
 Qed.
 
-Lemma nzhead_invol d : nzhead (nzhead d) = nzhead d.
+Lemma del_tail_nonnil n u :
+  n < nb_digits u -> del_tail n u <> Nil.
+Proof.
+  unfold del_tail.
+  rewrite <-nb_digits_rev.
+  generalize (rev u); clear u; intro u.
+  intros Hu H.
+  generalize (rev_nil_inv _ H); clear H.
+  now apply del_head_nonnil.
+Qed.
+
+Lemma nzhead_involutive d : nzhead (nzhead d) = nzhead d.
 Proof.
   now induction d.
 Qed.
+#[deprecated(since="8.13",note="Use nzhead_involutive instead.")]
+Notation nzhead_invol := nzhead_involutive (only parsing).
 
-Lemma nztail_invol d : nztail (nztail d) = nztail d.
+Lemma nztail_involutive 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.
+  now rewrite !rev_nztail_rev, nzhead_involutive.
 Qed.
+#[deprecated(since="8.13",note="Use nztail_involutive instead.")]
+Notation nztail_invol := nztail_involutive (only parsing).
 
-Lemma unorm_invol d : unorm (unorm d) = unorm d.
+Lemma unorm_involutive d : unorm (unorm d) = unorm d.
 Proof.
   unfold unorm.
   destruct (nzhead d) eqn:E; trivial.
   destruct (nzhead_nonzero _ _ E).
 Qed.
+#[deprecated(since="8.13",note="Use unorm_involutive instead.")]
+Notation unorm_invol := unorm_involutive (only parsing).
 
-Lemma norm_invol d : norm (norm d) = norm d.
+Lemma norm_involutive d : norm (norm d) = norm d.
 Proof.
   unfold norm.
   destruct d.
-  - f_equal. apply unorm_invol.
+  - f_equal. apply unorm_involutive.
   - destruct (nzhead d) eqn:E; auto.
     destruct (nzhead_nonzero _ _ E).
 Qed.
+#[deprecated(since="8.13",note="Use norm_involutive instead.")]
+Notation norm_invol := norm_involutive (only parsing).
+
+Lemma lnzhead_neq_d0_head l l' : ~(lnzhead l = cons d0 l').
+Proof. now induction l as [|h t Il]; [|case h]. Qed.
+
+Lemma lnzhead_head_nd0 h t : h <> d0 -> lnzhead (cons h t) = cons h t.
+Proof. now case h. Qed.
+
+Lemma nzhead_del_tail_nzhead_eq n u :
+  nzhead u = u ->
+  n < nb_digits u ->
+  nzhead (del_tail n u) = del_tail n u.
+Proof.
+  rewrite nb_digits_spec, <-List.rev_length.
+  intros Hu Hn.
+  apply to_list_inj; unfold del_tail.
+  rewrite nzhead_spec, rev_spec.
+  rewrite del_head_spec_small; [|now rewrite rev_spec; apply Nat.lt_le_incl].
+  rewrite rev_spec.
+  rewrite List.skipn_rev, List.rev_involutive.
+  generalize (f_equal to_list Hu) Hn; rewrite nzhead_spec; intro Hu'.
+  case (to_list u) as [|h t].
+  { simpl; intro H; exfalso; revert H; apply le_not_lt, Peano.le_0_n. }
+  intro Hn'; generalize (Nat.sub_gt _ _ Hn'); rewrite List.rev_length.
+  case (_ - _); [now simpl|]; intros n' _.
+  rewrite List.firstn_cons, lnzhead_head_nd0; [now simpl|].
+  intro Hh; revert Hu'; rewrite Hh; apply lnzhead_neq_d0_head.
+Qed.
+
+Lemma nzhead_del_tail_nzhead n u :
+  n < nb_digits (nzhead u) ->
+  nzhead (del_tail n (nzhead u)) = del_tail n (nzhead u).
+Proof. apply nzhead_del_tail_nzhead_eq, nzhead_involutive. Qed.
+
+Lemma unorm_del_tail_unorm n u :
+  n < nb_digits (unorm u) ->
+  unorm (del_tail n (unorm u)) = del_tail n (unorm u).
+Proof.
+  case (uint_eq_dec (nzhead u) Nil).
+  - unfold unorm; intros->; case n; [now simpl|]; intro n'.
+    now simpl; intro H; exfalso; generalize (lt_S_n _ _ H).
+  - unfold unorm.
+    set (m := match nzhead u with Nil => zero | _ => _ end).
+    intros H.
+    replace m with (nzhead u).
+    + intros H'.
+      rewrite (nzhead_del_tail_nzhead _ _ H').
+      now generalize (del_tail_nonnil _ _ H'); case del_tail.
+    + now unfold m; revert H; case nzhead.
+Qed.
+
+Lemma norm_del_tail_int_norm n d :
+  n < nb_digits (match norm d with Pos d | Neg d => d end) ->
+  norm (del_tail_int n (norm d)) = del_tail_int n (norm d).
+Proof.
+  case d; clear d; intros u; simpl.
+  - now intro H; simpl; rewrite unorm_del_tail_unorm.
+  - case (uint_eq_dec (nzhead u) Nil); intro Hu.
+    + now rewrite Hu; case n; [|intros n' Hn'; generalize (lt_S_n _ _ Hn')].
+    + set (m := match nzhead u with Nil => Pos zero | _ => _ end).
+      replace m with (Neg (nzhead u)); [|now unfold m; revert Hu; case nzhead].
+      unfold del_tail_int.
+      clear m Hu.
+      simpl.
+      intro H; generalize (del_tail_nonnil _ _ H).
+      rewrite (nzhead_del_tail_nzhead _ _ H).
+      now case del_tail.
+Qed.
 
 Lemma nzhead_app_nzhead d d' :
   nzhead (app (nzhead d) d') = nzhead (app d d').
@@ -299,7 +684,7 @@ Proof.
   generalize (nzhead_revapp d d').
   generalize (nzhead_revapp_0 (nztail d) d').
   generalize (nzhead_revapp (nztail d) d').
-  rewrite nztail_invol.
+  rewrite nztail_involutive.
   now case nztail;
     [intros _ H _ H'; rewrite (H eq_refl), (H' eq_refl)
     |intros d'' H _ H' _; rewrite H; [rewrite H'|]..].
@@ -336,5 +721,5 @@ Proof.
        |rewrite H'; unfold r; clear m r H'];
        unfold norm;
        rewrite rev_rev, <-Hd'';
-       rewrite nzhead_revapp; rewrite nztail_invol; [|rewrite Hd'']..].
+       rewrite nzhead_revapp; rewrite nztail_involutive; [|rewrite Hd'']..].
 Qed.
diff --git a/theories/Numbers/HexadecimalN.v b/theories/Numbers/HexadecimalN.v
index f333e2b7f6..93ba82d14a 100644
--- a/theories/Numbers/HexadecimalN.v
+++ b/theories/Numbers/HexadecimalN.v
@@ -74,7 +74,7 @@ Proof.
   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.
+  - intros [= <-]. apply unorm_involutive.
   - destruct (nzhead d); now intros [= <-].
 Qed.
 
@@ -93,7 +93,7 @@ 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.
+  unfold N.of_hex_int. now rewrite norm_involutive.
 Qed.
 
 Lemma of_inj_pos d d' :
diff --git a/theories/Numbers/HexadecimalNat.v b/theories/Numbers/HexadecimalNat.v
index b05184e821..94a14b90bd 100644
--- a/theories/Numbers/HexadecimalNat.v
+++ b/theories/Numbers/HexadecimalNat.v
@@ -289,7 +289,7 @@ Proof.
   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.
+  - intros [= <-]. apply unorm_involutive.
   - destruct (nzhead d); now intros [= <-].
 Qed.
 
@@ -308,7 +308,7 @@ 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.
+  unfold Nat.of_hex_int. now rewrite norm_involutive.
 Qed.
 
 Lemma of_inj_pos d d' :
diff --git a/theories/Numbers/HexadecimalQ.v b/theories/Numbers/HexadecimalQ.v
index 9bf43ceb88..a32019767c 100644
--- a/theories/Numbers/HexadecimalQ.v
+++ b/theories/Numbers/HexadecimalQ.v
@@ -16,442 +16,412 @@
 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.
+Lemma of_IQmake_to_hexadecimal num den :
+  match IQmake_to_hexadecimal num den with
+  | None => True
+  | Some (HexadecimalExp _ _ _) => False
+  | Some (Hexadecimal i f) => of_hexadecimal (Hexadecimal i f) = IQmake (IZ_of_Z num) den
+  end.
+Proof.
+  unfold IQmake_to_hexadecimal.
+  generalize (Unsigned.nztail_to_hex_uint den).
+  case Hexadecimal.nztail; intros den' e_den'.
+  case den'; [now simpl|now simpl| |now simpl..]; clear den'; intro den'.
+  case den'; [ |now simpl..]; clear den'.
+  case e_den' as [|e_den']; simpl; intro H; injection H; clear H; intros->.
+  { now unfold of_hexadecimal; simpl; rewrite app_int_nil_r, HexadecimalZ.of_to. }
+  replace (16 ^ _)%positive with (Nat.iter (S e_den') (Pos.mul 16) 1%positive).
+  2:{ induction e_den' as [|n IHn]; [now simpl| ].
+    now rewrite SuccNat2Pos.inj_succ, Pos.pow_succ_r, <-IHn. }
+  case Nat.ltb_spec; intro He_den'.
+  - unfold of_hexadecimal; simpl.
+    rewrite app_int_del_tail_head; [|now apply Nat.lt_le_incl].
+    rewrite HexadecimalZ.of_to.
+    now rewrite nb_digits_del_head_sub; [|now apply Nat.lt_le_incl].
+  - unfold of_hexadecimal; simpl.
+    rewrite nb_digits_iter_D0.
+    apply f_equal2.
+    + apply f_equal, HexadecimalZ.to_int_inj.
+      rewrite HexadecimalZ.to_of.
+      rewrite <-(HexadecimalZ.of_to num), HexadecimalZ.to_of.
+      case (Z.to_hex_int num); clear He_den' num; intro num; simpl.
+      * unfold app; simpl.
+        now rewrite unorm_D0, unorm_iter_D0, unorm_involutive.
+      * case (uint_eq_dec (nzhead num) Nil); [|intro Hn].
+        { intros->; simpl; unfold app; simpl.
+          now rewrite unorm_D0, unorm_iter_D0. }
+        replace (match nzhead num with Nil => _ | _ => _ end)
+          with (Neg (nzhead num)); [|now revert Hn; case nzhead].
+        simpl.
+        rewrite nzhead_iter_D0, nzhead_involutive.
+        now revert Hn; case nzhead.
+    + revert He_den'; case nb_digits as [|n]; [now simpl; rewrite Nat.add_0_r|].
+      intro Hn.
+      rewrite Nat.add_succ_r, Nat.add_comm.
+      now rewrite <-le_plus_minus; [|apply le_S_n].
+Qed.
+
+Lemma IZ_of_Z_IZ_to_Z z z' : IZ_to_Z z = Some z' -> IZ_of_Z z' = z.
+Proof. now case z as [| |p|p]; [|intro H; injection H; intros<-..]. Qed.
+
+Lemma of_IQmake_to_hexadecimal' num den :
+  match IQmake_to_hexadecimal' num den with
+  | None => True
+  | Some (HexadecimalExp _ _ _) => False
+  | Some (Hexadecimal i f) => of_hexadecimal (Hexadecimal i f) = IQmake num den
+  end.
+Proof.
+  unfold IQmake_to_hexadecimal'.
+  case_eq (IZ_to_Z num); [intros num' Hnum'|now simpl].
+  generalize (of_IQmake_to_hexadecimal num' den).
+  case IQmake_to_hexadecimal as [d|]; [|now simpl].
+  case d as [i f|]; [|now simpl].
+  now rewrite (IZ_of_Z_IZ_to_Z _ _ Hnum').
+Qed.
+
+Lemma of_to (q:IQ) : 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|].
+  intro d.
+  case q as [num den|q q'|q q']; simpl.
+  - generalize (of_IQmake_to_hexadecimal' num den).
+    case IQmake_to_hexadecimal' as [d'|]; [|now simpl].
+    case d' as [i f|]; [|now simpl].
+    now intros H H'; injection H'; clear H'; intros <-.
+  - case q as [num den| |]; [|now simpl..].
+    case q' as [num' den'| |]; [|now simpl..].
+    case num' as [z p| | |]; [|now simpl..].
+    case (Z.eq_dec z 2); [intros->|].
+    2:{ case z; [now simpl| |now simpl]; intro pz'.
+      case pz'; [intros d0..| ]; [now simpl| |now simpl].
+      now case d0. }
+    case (Pos.eq_dec den' 1%positive); [intros->|now case den'].
+    generalize (of_IQmake_to_hexadecimal' num den).
+    case IQmake_to_hexadecimal' as [d'|]; [|now simpl].
+    case d' as [i f|]; [|now simpl].
+    intros <-; clear num den.
+    intros H; injection H; clear H; intros<-.
+    unfold of_hexadecimal; simpl.
+    now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
+  - case q as [num den| |]; [|now simpl..].
+    case q' as [num' den'| |]; [|now simpl..].
+    case num' as [z p| | |]; [|now simpl..].
+    case (Z.eq_dec z 2); [intros->|].
+    2:{ case z; [now simpl| |now simpl]; intro pz'.
+      case pz'; [intros d0..| ]; [now simpl| |now simpl].
+      now case d0. }
+    case (Pos.eq_dec den' 1%positive); [intros->|now case den'].
+    generalize (of_IQmake_to_hexadecimal' num den).
+    case IQmake_to_hexadecimal' as [d'|]; [|now simpl].
+    case d' as [i f|]; [|now simpl].
+    intros <-; clear num den.
+    intros H; injection H; clear H; intros<-.
+    unfold of_hexadecimal; simpl.
+    now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
 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)
+
+Definition dnorm (d:hexadecimal) : hexadecimal :=
+  let norm_i i f :=
+    match i with
+    | Pos i => Pos (unorm i)
+    | Neg i => match nzhead (app i f) with Nil => Pos zero | _ => Neg (unorm i) end
     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))
+  match d with
+  | Hexadecimal i f => Hexadecimal (norm_i i f) f
+  | HexadecimalExp i f e =>
+    match Decimal.norm e with
+    | Decimal.Pos Decimal.zero => Hexadecimal (norm_i i f) f
+    | e => HexadecimalExp (norm_i i f) f e
+    end
   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
+Lemma dnorm_spec_i d :
+  let (i, f) :=
+    match d with Hexadecimal i f => (i, f) | HexadecimalExp i f _ => (i, f) end in
+  let i' := match dnorm d with Hexadecimal i _ => i | HexadecimalExp i _ _ => i end in
+  match i with
+  | Pos i => i' = Pos (unorm i)
+  | Neg i =>
+    (i' = Neg (unorm i) /\ (nzhead i <> Nil \/ nzhead f <> Nil))
+    \/ (i' = Pos zero /\ (nzhead i = Nil /\ nzhead f = Nil))
   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).
+  case d as [i f|i f e]; case i as [i|i].
+  - now simpl.
+  - simpl; case (uint_eq_dec (nzhead (app i f)) Nil); intro Ha.
+    + rewrite Ha; right; split; [now simpl|split].
+      * now unfold unorm; rewrite (nzhead_app_nil_l _ _ Ha).
+      * now unfold unorm; rewrite (nzhead_app_nil_r _ _ Ha).
+    + left; split; [now revert Ha; case nzhead|].
+      case (uint_eq_dec (nzhead i) Nil).
+      * intro Hi; right; intro Hf; apply Ha.
+        now rewrite <-nzhead_app_nzhead, Hi, app_nil_l.
+      * now intro H; left.
+  - simpl; case (Decimal.norm e); clear e; intro e; [|now simpl].
+    now case e; clear e; [|intro e..]; [|case e|..].
+  - simpl.
+    set (m := match nzhead _ with Nil => _ | _ => _ end).
+    set (m' := match _ with Hexadecimal _ _ => _ | _ => _ end).
+    replace m' with m.
+    2:{ unfold m'; case (Decimal.norm e); clear m' e; intro e; [|now simpl].
+      now case e; clear e; [|intro e..]; [|case e|..]. }
+    unfold m; case (uint_eq_dec (nzhead (app i f)) Nil); intro Ha.
+    + rewrite Ha; right; split; [now simpl|split].
+      * now unfold unorm; rewrite (nzhead_app_nil_l _ _ Ha).
+      * now unfold unorm; rewrite (nzhead_app_nil_r _ _ Ha).
+    + left; split; [now revert Ha; case nzhead|].
+      case (uint_eq_dec (nzhead i) Nil).
+      * intro Hi; right; intro Hf; apply Ha.
+        now rewrite <-nzhead_app_nzhead, Hi, app_nil_l.
+      * now intro H; left.
 Qed.
 
-Lemma hnorme_invol d : hnorme (hnorme d) = hnorme d.
+Lemma dnorm_spec_f d :
+  let f := match d with Hexadecimal _ f => f | HexadecimalExp _ f _ => f end in
+  let f' := match dnorm d with Hexadecimal _ f => f | HexadecimalExp _ f _ => f end in
+  f' = f.
+Proof.
+  case d as [i f|i f e]; [now simpl|].
+  simpl; case (Decimal.int_eq_dec (Decimal.norm e) (Decimal.Pos Decimal.zero)); [now intros->|intro He].
+  set (i' := match i with Pos _ => _ | _ => _ end).
+  set (m := match Decimal.norm e with Decimal.Pos _ => _ | _ => _ end).
+  replace m with (HexadecimalExp i' f (Decimal.norm e)); [now simpl|].
+  unfold m; revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl].
+  now case e; clear e; [|intro e; case e|..].
+Qed.
+
+Lemma dnorm_spec_e d :
+  match d, dnorm d with
+    | Hexadecimal _ _, Hexadecimal _ _ => True
+    | HexadecimalExp _ _ e, Hexadecimal _ _ =>
+      Decimal.norm e = Decimal.Pos Decimal.zero
+    | HexadecimalExp _ _ e, HexadecimalExp _ _ e' =>
+      e' = Decimal.norm e /\ e' <> Decimal.Pos Decimal.zero
+    | Hexadecimal _ _, HexadecimalExp _ _ _ => False
+  end.
 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.
+  case d as [i f|i f e]; [now simpl|].
+  simpl; case (Decimal.int_eq_dec (Decimal.norm e) (Decimal.Pos Decimal.zero)); [now intros->|intro He].
+  set (i' := match i with Pos _ => _ | _ => _ end).
+  set (m := match Decimal.norm e with Decimal.Pos _ => _ | _ => _ end).
+  replace m with (HexadecimalExp i' f (Decimal.norm e)); [now simpl|].
+  unfold m; revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl].
+  now case e; clear e; [|intro e; case e|..].
 Qed.
 
-Lemma to_of (d:hexadecimal) :
-  to_hexadecimal (of_hexadecimal d) = Some (hnorme d).
+Lemma dnorm_involutive d : dnorm (dnorm d) = dnorm 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.
+  case d as [i f|i f e]; case i as [i|i].
+  - now simpl; rewrite unorm_involutive.
+  - simpl; case (uint_eq_dec (nzhead (app i f)) Nil); [now intros->|intro Ha].
+    set (m := match nzhead _ with Nil =>_ | _ => _ end).
+    replace m with (Neg (unorm i)).
+    2:{ now unfold m; revert Ha; case nzhead. }
+    case (uint_eq_dec (nzhead i) Nil); intro Hi.
+    + unfold unorm; rewrite Hi; simpl.
+      case (uint_eq_dec (nzhead f) Nil).
+      * intro Hf; exfalso; apply Ha.
+        now rewrite <-nzhead_app_nzhead, Hi, app_nil_l.
+      * now case nzhead.
+    + rewrite unorm_involutive, (unorm_nzhead _ Hi), nzhead_app_nzhead.
+      now revert Ha; case nzhead.
+  - simpl; case (Decimal.int_eq_dec (Decimal.norm e) (Decimal.Pos Decimal.zero)); intro He.
+    + now rewrite He; simpl; rewrite unorm_involutive.
+    + set (m := match Decimal.norm e with Decimal.Pos _ => _ | _ => _ end).
+      replace m with (HexadecimalExp (Pos (unorm i)) f (Decimal.norm e)).
+      2:{ unfold m; revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl].
+        now case e; clear e; [|intro e; case e|..]. }
+      simpl; rewrite DecimalFacts.norm_involutive, unorm_involutive.
+      revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl].
+      now case e; clear e; [|intro e; case e|..].
+  - simpl; case (Decimal.int_eq_dec (Decimal.norm e) (Decimal.Pos Decimal.zero)); intro He.
+    + rewrite He; simpl.
+      case (uint_eq_dec (nzhead (app i f)) Nil); [now intros->|intro Ha].
+      set (m := match nzhead _ with Nil =>_ | _ => _ end).
+      replace m with (Neg (unorm i)).
+      2:{ now unfold m; revert Ha; case nzhead. }
+      case (uint_eq_dec (nzhead i) Nil); intro Hi.
+      * unfold unorm; rewrite Hi; simpl.
+        case (uint_eq_dec (nzhead f) Nil).
+        -- intro Hf; exfalso; apply Ha.
+           now rewrite <-nzhead_app_nzhead, Hi, app_nil_l.
+        -- now case nzhead.
+      * rewrite unorm_involutive, (unorm_nzhead _ Hi), nzhead_app_nzhead.
+        now revert Ha; case nzhead.
+    + set (m := match Decimal.norm e with Decimal.Pos _ => _ | _ => _ end).
+      pose (i' := match nzhead (app i f) with Nil => Pos zero | _ => Neg (unorm i) end).
+      replace m with (HexadecimalExp i' f (Decimal.norm e)).
+      2:{ unfold m; revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl].
+        now case e; clear e; [|intro e; case e|..]. }
+      simpl; rewrite DecimalFacts.norm_involutive.
+      set (i'' := match i' with Pos _ => _ | _ => _ end).
+      clear m; set (m := match Decimal.norm e with Decimal.Pos _ => _ | _ => _ end).
+      replace m with (HexadecimalExp i'' f (Decimal.norm e)).
+      2:{ unfold m; revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl].
+        now case e; clear e; [|intro e; case e|..]. }
+      unfold i'', i'.
+      case (uint_eq_dec (nzhead (app i f)) Nil); [now intros->|intro Ha].
+      fold i'; replace i' with (Neg (unorm i)).
+      2:{ now unfold i'; revert Ha; case nzhead. }
+      case (uint_eq_dec (nzhead i) Nil); intro Hi.
+      * unfold unorm; rewrite Hi; simpl.
+        case (uint_eq_dec (nzhead f) Nil).
+        -- intro Hf; exfalso; apply Ha.
+           now rewrite <-nzhead_app_nzhead, Hi, app_nil_l.
+        -- now case nzhead.
+      * rewrite unorm_involutive, (unorm_nzhead _ Hi), nzhead_app_nzhead.
+        now revert Ha; case nzhead.
+Qed.
+
+Lemma IZ_to_Z_IZ_of_Z z : IZ_to_Z (IZ_of_Z z) = Some z.
+Proof. now case z. Qed.
+
+Lemma dnorm_i_exact i f :
+  (nb_digits f < nb_digits (unorm (app (abs i) f)))%nat ->
+  match i with
+  | Pos i => Pos (unorm i)
+  | Neg i =>
+    match nzhead (app i f) with
+    | Nil => Pos zero
+    | _ => Neg (unorm i)
+    end
+  end = norm i.
+Proof.
+  case i as [ni|ni]; [now simpl|]; simpl.
+  case (uint_eq_dec (nzhead (app ni f)) Nil); intro Ha.
+  { now rewrite Ha, (nzhead_app_nil_l _ _ Ha). }
+  rewrite (unorm_nzhead _ Ha).
+  set (m := match nzhead _ with Nil => _ | _ => _ end).
+  replace m with (Neg (unorm ni)); [|now unfold m; revert Ha; case nzhead].
+  case (uint_eq_dec (nzhead ni) Nil); intro Hni.
+  { rewrite <-nzhead_app_nzhead, Hni, app_nil_l.
+    intro H; exfalso; revert H; apply le_not_lt, nb_digits_nzhead. }
+  clear m; set (m := match nzhead ni with Nil => _ | _ => _ end).
+  replace m with (Neg (nzhead ni)); [|now unfold m; revert Hni; case nzhead].
+  now rewrite (unorm_nzhead _ Hni).
+Qed.
+
+Lemma dnorm_i_exact' i f :
+  (nb_digits (unorm (app (abs i) f)) <= nb_digits f)%nat ->
+  match i with
+  | Pos i => Pos (unorm i)
+  | Neg i =>
+    match nzhead (app i f) with
+    | Nil => Pos zero
+    | _ => Neg (unorm i)
+    end
+  end =
+  match norm (app_int i f) with
+  | Pos _ => Pos zero
+  | Neg _ => Neg zero
+  end.
+Proof.
+  case i as [ni|ni]; simpl.
+  { now intro Hnb; rewrite (unorm_app_zero _ _ Hnb). }
+  unfold unorm.
+  case (uint_eq_dec (nzhead (app ni f)) Nil); intro Hn.
+  { now rewrite Hn. }
+  set (m := match nzhead _ with Nil => _ | _ => _ end).
+  replace m with (nzhead (app ni f)).
+  2:{ now unfold m; revert Hn; case nzhead. }
+  clear m; set (m := match nzhead _ with Nil => _ | _ => _ end).
+  replace m with (Neg (unorm ni)).
+  2:{ now unfold m, unorm; revert Hn; case nzhead. }
+  clear m; set (m := match nzhead _ with Nil => _ | _ => _ end).
+  replace m with (Neg (nzhead (app ni f))).
+  2:{ now unfold m; revert Hn; case nzhead. }
+  rewrite <-(unorm_nzhead _ Hn).
+  now intro H; rewrite (unorm_app_zero _ _ H).
+Qed.
+
+Lemma to_of (d:hexadecimal) : to_hexadecimal (of_hexadecimal d) = Some (dnorm d).
+Proof.
+  case d as [i f|i f e].
+  - unfold of_hexadecimal; simpl; unfold IQmake_to_hexadecimal'.
+    rewrite IZ_to_Z_IZ_of_Z.
+    unfold IQmake_to_hexadecimal; simpl.
+    change (fun _ : positive => _) with (Pos.mul 16).
+    rewrite nztail_to_hex_uint_pow16, to_of.
+    case_eq (nb_digits f); [|intro nb]; intro Hnb.
+    + rewrite (nb_digits_0 _ Hnb), app_int_nil_r.
+      case i as [ni|ni]; [now simpl|].
+      rewrite app_nil_r; simpl; unfold unorm.
+      now case (nzhead ni).
+    + rewrite <-Hnb.
+      rewrite abs_norm, abs_app_int.
+      case Nat.ltb_spec; intro Hnb'.
+      * rewrite (del_tail_app_int_exact _ _ Hnb').
+        rewrite (del_head_app_int_exact _ _ Hnb').
+        now rewrite (dnorm_i_exact _ _ Hnb').
+      * rewrite (unorm_app_r _ _ Hnb').
+        rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb].
+        now rewrite dnorm_i_exact'.
+  - unfold of_hexadecimal; simpl.
+    rewrite <-DecimalZ.to_of.
+    case (Z.of_int e); clear e; [|intro e..]; simpl.
+    + unfold IQmake_to_hexadecimal'.
+      rewrite IZ_to_Z_IZ_of_Z.
+      unfold IQmake_to_hexadecimal; simpl.
+      change (fun _ : positive => _) with (Pos.mul 16).
+      rewrite nztail_to_hex_uint_pow16, to_of.
+      case_eq (nb_digits f); [|intro nb]; intro Hnb.
+      * rewrite (nb_digits_0 _ Hnb), app_int_nil_r.
+        case i as [ni|ni]; [now simpl|].
+        rewrite app_nil_r; simpl; unfold unorm.
+        now case (nzhead ni).
+      * rewrite <-Hnb.
+        rewrite abs_norm, abs_app_int.
+        case Nat.ltb_spec; intro Hnb'.
+        -- rewrite (del_tail_app_int_exact _ _ Hnb').
+           rewrite (del_head_app_int_exact _ _ Hnb').
+           now rewrite (dnorm_i_exact _ _ Hnb').
+        -- rewrite (unorm_app_r _ _ Hnb').
+           rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb].
+           now rewrite dnorm_i_exact'.
+    + unfold IQmake_to_hexadecimal'.
+      rewrite IZ_to_Z_IZ_of_Z.
+      unfold IQmake_to_hexadecimal; simpl.
+      change (fun _ : positive => _) with (Pos.mul 16).
+      rewrite nztail_to_hex_uint_pow16, to_of.
+      generalize (DecimalPos.Unsigned.to_uint_nonzero e); intro He.
+      set (dnorm_i := match i with Pos _ => _ | _ => _ end).
+      set (m := match Pos.to_uint e with Decimal.Nil => _ | _ => _ end).
+      replace m with (HexadecimalExp dnorm_i f (Decimal.Pos (Pos.to_uint e))).
+      2:{ now unfold m; revert He; case (Pos.to_uint e); [|intro u; case u|..]. }
+      clear m; unfold dnorm_i.
+      case_eq (nb_digits f); [|intro nb]; intro Hnb.
+      * rewrite (nb_digits_0 _ Hnb), app_int_nil_r.
+        case i as [ni|ni]; [now simpl|].
+        rewrite app_nil_r; simpl; unfold unorm.
+        now case (nzhead ni).
+      * rewrite <-Hnb.
+        rewrite abs_norm, abs_app_int.
+        case Nat.ltb_spec; intro Hnb'.
+        -- rewrite (del_tail_app_int_exact _ _ Hnb').
+           rewrite (del_head_app_int_exact _ _ Hnb').
+           now rewrite (dnorm_i_exact _ _ Hnb').
+        -- rewrite (unorm_app_r _ _ Hnb').
+           rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb].
+           now rewrite dnorm_i_exact'.
+    + unfold IQmake_to_hexadecimal'.
+      rewrite IZ_to_Z_IZ_of_Z.
+      unfold IQmake_to_hexadecimal; simpl.
+      change (fun _ : positive => _) with (Pos.mul 16).
+      rewrite nztail_to_hex_uint_pow16, to_of.
+      case_eq (nb_digits f); [|intro nb]; intro Hnb.
+      * rewrite (nb_digits_0 _ Hnb), app_int_nil_r.
+        case i as [ni|ni]; [now simpl|].
+        rewrite app_nil_r; simpl; unfold unorm.
+        now case (nzhead ni).
+      * rewrite <-Hnb.
+        rewrite abs_norm, abs_app_int.
+        case Nat.ltb_spec; intro Hnb'.
+        -- rewrite (del_tail_app_int_exact _ _ Hnb').
+           rewrite (del_head_app_int_exact _ _ Hnb').
+           now rewrite (dnorm_i_exact _ _ Hnb').
+        -- rewrite (unorm_app_r _ _ Hnb').
+           rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb].
+           now rewrite dnorm_i_exact'.
 Qed.
 
 (** Some consequences *)
@@ -466,68 +436,24 @@ Proof.
   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).
+Lemma to_hexadecimal_surj d : exists q, to_hexadecimal q = Some (dnorm 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_hexadecimal_dnorm d : of_hexadecimal (dnorm d) = of_hexadecimal d.
+Proof. now apply to_hexadecimal_inj; rewrite !to_of; [|rewrite dnorm_involutive]. Qed.
 
-Lemma of_inj d d' :
-  of_hexadecimal d = of_hexadecimal d' -> hnorme d = hnorme d'.
+Lemma of_inj d d' : of_hexadecimal d = of_hexadecimal d' -> dnorm d = dnorm d'.
 Proof.
-  intros.
-  cut (Some (hnorme d) = Some (hnorme d')); [now intro H'; injection H'|].
-  rewrite <- !to_of. now f_equal.
+  intro H.
+  apply (@f_equal _ _ (fun x => match x with Some x => x | _ => d end)
+                  (Some (dnorm d)) (Some (dnorm d'))).
+  now rewrite <- !to_of, H.
 Qed.
 
-Lemma of_iff d d' :
-  of_hexadecimal d = of_hexadecimal d' <-> hnorme d = hnorme d'.
+Lemma of_iff d d' : of_hexadecimal d = of_hexadecimal d' <-> dnorm d = dnorm d'.
 Proof.
-  split. apply of_inj. intros E. rewrite <- of_hexadecimal_hnorme, E.
-  apply of_hexadecimal_hnorme.
+  split. apply of_inj. intros E. rewrite <- of_hexadecimal_dnorm, E.
+  apply of_hexadecimal_dnorm.
 Qed.
diff --git a/theories/Numbers/HexadecimalR.v b/theories/Numbers/HexadecimalR.v
new file mode 100644
index 0000000000..2deecc5847
--- /dev/null
+++ b/theories/Numbers/HexadecimalR.v
@@ -0,0 +1,302 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+(** * HexadecimalR
+
+    Proofs that conversions between hexadecimal numbers and [R]
+    are bijections. *)
+
+Require Import Decimal DecimalFacts.
+Require Import Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalZ.
+Require Import HexadecimalQ Rdefinitions.
+
+Lemma of_IQmake_to_hexadecimal num den :
+  match IQmake_to_hexadecimal num den with
+  | None => True
+  | Some (HexadecimalExp _ _ _) => False
+  | Some (Hexadecimal i f) =>
+    of_hexadecimal (Hexadecimal i f) = IRQ (QArith_base.Qmake num den)
+  end.
+Proof.
+  unfold IQmake_to_hexadecimal.
+  case (Pos.eq_dec den 1); [now intros->|intro Hden].
+  assert (Hf : match QArith_base.IQmake_to_hexadecimal num den with
+               | Some (Hexadecimal i f) => f <> Nil
+               | _ => True
+               end).
+  { unfold QArith_base.IQmake_to_hexadecimal; simpl.
+    generalize (Unsigned.nztail_to_hex_uint den).
+    case Hexadecimal.nztail as [den' e_den'].
+    case den'; [now simpl|now simpl| |now simpl..]; clear den'; intro den'.
+    case den'; [ |now simpl..]; clear den'.
+    case e_den' as [|e_den']; [now simpl; intros H _; apply Hden; injection H|].
+    intros _.
+    case Nat.ltb_spec; intro He_den'.
+    - apply del_head_nonnil.
+      revert He_den'; case nb_digits as [|n]; [now simpl|].
+      now intro H; simpl; apply le_lt_n_Sm, Nat.le_sub_l.
+    - apply nb_digits_n0.
+      now rewrite nb_digits_iter_D0, Nat.sub_add. }
+  replace (match den with 1%positive => _ | _ => _ end)
+    with (QArith_base.IQmake_to_hexadecimal num den); [|now revert Hden; case den].
+  generalize (of_IQmake_to_hexadecimal num den).
+  case QArith_base.IQmake_to_hexadecimal as [d'|]; [|now simpl].
+  case d' as [i f|]; [|now simpl].
+  unfold of_hexadecimal; simpl.
+  intro H; injection H; clear H; intros <-.
+  intro H; generalize (f_equal QArith_base.IZ_to_Z H); clear H.
+  rewrite !IZ_to_Z_IZ_of_Z; intro H; injection H; clear H; intros<-.
+  now revert Hf; case f.
+Qed.
+
+Lemma of_to (q:IR) : forall d, to_hexadecimal q = Some d -> of_hexadecimal d = q.
+Proof.
+  intro d.
+  case q as [z|q|r r'|r r']; simpl.
+  - case z as [z p| |p|p].
+    + now simpl.
+    + now simpl; intro H; injection H; clear H; intros<-.
+    + simpl; intro H; injection H; clear H; intros<-.
+      now unfold of_hexadecimal; simpl; unfold Z.of_hex_uint; rewrite Unsigned.of_to.
+    + simpl; intro H; injection H; clear H; intros<-.
+      now unfold of_hexadecimal; simpl; unfold Z.of_hex_uint; rewrite Unsigned.of_to.
+  - case q as [num den].
+    generalize (of_IQmake_to_hexadecimal num den).
+    case IQmake_to_hexadecimal as [d'|]; [|now simpl].
+    case d' as [i f|]; [|now simpl].
+    now intros H H'; injection H'; intros<-.
+  - case r as [z|q| |]; [|case q as[num den]|now simpl..];
+      (case r' as [z'| | |]; [|now simpl..]);
+      (case z' as [p e| | |]; [|now simpl..]).
+    + case (Z.eq_dec p 2); [intros->|intro Hp].
+      2:{ now revert Hp; case p;
+          [|intro d0; case d0; [intro d1..|]; [|case d1|]..]. }
+      case z as [| |p|p]; [now simpl|..]; intro H; injection H; intros<-.
+      * now unfold of_hexadecimal; simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to.
+      * unfold of_hexadecimal; simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
+        now unfold Z.of_hex_uint; rewrite Unsigned.of_to.
+      * unfold of_hexadecimal; simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
+        now unfold Z.of_hex_uint; rewrite Unsigned.of_to.
+    + case (Z.eq_dec p 2); [intros->|intro Hp].
+      2:{ now revert Hp; case p;
+          [|intro d0; case d0; [intro d1..|]; [|case d1|]..]. }
+      generalize (of_IQmake_to_hexadecimal num den).
+      case IQmake_to_hexadecimal as [d'|]; [|now simpl].
+      case d' as [i f|]; [|now simpl].
+      intros H H'; injection H'; clear H'; intros<-.
+      unfold of_hexadecimal; simpl.
+      change (match f with Nil => _ | _ => _ end) with (of_hexadecimal (Hexadecimal i f)).
+      rewrite H; clear H.
+      now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to.
+  - case r as [z|q| |]; [|case q as[num den]|now simpl..];
+      (case r' as [z'| | |]; [|now simpl..]);
+      (case z' as [p e| | |]; [|now simpl..]).
+    + case (Z.eq_dec p 2); [intros->|intro Hp].
+      2:{ now revert Hp; case p;
+          [|intro d0; case d0; [intro d1..|]; [|case d1|]..]. }
+      case z as [| |p|p]; [now simpl|..]; intro H; injection H; intros<-.
+      * now unfold of_hexadecimal; simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to.
+      * unfold of_hexadecimal; simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
+        now unfold Z.of_hex_uint; rewrite Unsigned.of_to.
+      * unfold of_hexadecimal; simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
+        now unfold Z.of_hex_uint; rewrite Unsigned.of_to.
+    + case (Z.eq_dec p 2); [intros->|intro Hp].
+      2:{ now revert Hp; case p;
+          [|intro d0; case d0; [intro d1..|]; [|case d1|]..]. }
+      generalize (of_IQmake_to_hexadecimal num den).
+      case IQmake_to_hexadecimal as [d'|]; [|now simpl].
+      case d' as [i f|]; [|now simpl].
+      intros H H'; injection H'; clear H'; intros<-.
+      unfold of_hexadecimal; simpl.
+      change (match f with Nil => _ | _ => _ end) with (of_hexadecimal (Hexadecimal i f)).
+      rewrite H; clear H.
+      now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to.
+Qed.
+
+Lemma to_of (d:hexadecimal) : to_hexadecimal (of_hexadecimal d) = Some (dnorm d).
+Proof.
+  case d as [i f|i f e].
+  - unfold of_hexadecimal; simpl.
+    case (uint_eq_dec f Nil); intro Hf.
+    + rewrite Hf; clear f Hf.
+      unfold to_hexadecimal; simpl.
+      rewrite IZ_to_Z_IZ_of_Z, HexadecimalZ.to_of.
+      case i as [i|i]; [now simpl|]; simpl.
+      rewrite app_nil_r.
+      case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi].
+      now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead.
+    + set (r := IRQ _).
+      set (m := match f with Nil => _ | _ => _ end).
+      replace m with r; [unfold r|now unfold m; revert Hf; case f].
+      unfold to_hexadecimal; simpl.
+      unfold IQmake_to_hexadecimal; simpl.
+      set (n := Nat.iter _ _ _).
+      case (Pos.eq_dec n 1); intro Hn.
+      exfalso; apply Hf.
+      { now apply nb_digits_0; revert Hn; unfold n; case nb_digits. }
+      clear m; set (m := match n with 1%positive | _ => _ end).
+      replace m with (QArith_base.IQmake_to_hexadecimal (Z.of_hex_int (app_int i f)) n).
+      2:{ now unfold m; revert Hn; case n. }
+      unfold QArith_base.IQmake_to_hexadecimal, n; simpl.
+      rewrite nztail_to_hex_uint_pow16.
+      clear r; set (r := if _ <? _ then Some (Hexadecimal _ _) else Some _).
+      clear m; set (m := match nb_digits f with 0 => _ | _ => _ end).
+      replace m with r; [unfold r|now unfold m; revert Hf; case f].
+      rewrite HexadecimalZ.to_of, abs_norm, abs_app_int.
+      case Nat.ltb_spec; intro Hnf.
+      * rewrite (del_tail_app_int_exact _ _ Hnf).
+        rewrite (del_head_app_int_exact _ _ Hnf).
+        now rewrite (dnorm_i_exact _ _ Hnf).
+      * rewrite (unorm_app_r _ _ Hnf).
+        rewrite (iter_D0_unorm _ Hf).
+        now rewrite dnorm_i_exact'.
+  - unfold of_hexadecimal; simpl.
+    rewrite <-(DecimalZ.to_of e).
+    case (Z.of_int e); clear e; [|intro e..]; simpl.
+    + case (uint_eq_dec f Nil); intro Hf.
+      * rewrite Hf; clear f Hf.
+        unfold to_hexadecimal; simpl.
+        rewrite IZ_to_Z_IZ_of_Z, HexadecimalZ.to_of.
+        case i as [i|i]; [now simpl|]; simpl.
+        rewrite app_nil_r.
+        case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi].
+        now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead.
+      * set (r := IRQ _).
+        set (m := match f with Nil => _ | _ => _ end).
+        replace m with r; [unfold r|now unfold m; revert Hf; case f].
+        unfold to_hexadecimal; simpl.
+        unfold IQmake_to_hexadecimal; simpl.
+        set (n := Nat.iter _ _ _).
+        case (Pos.eq_dec n 1); intro Hn.
+        exfalso; apply Hf.
+        { now apply nb_digits_0; revert Hn; unfold n; case nb_digits. }
+        clear m; set (m := match n with 1%positive | _ => _ end).
+        replace m with (QArith_base.IQmake_to_hexadecimal (Z.of_hex_int (app_int i f)) n).
+        2:{ now unfold m; revert Hn; case n. }
+        unfold QArith_base.IQmake_to_hexadecimal, n; simpl.
+        rewrite nztail_to_hex_uint_pow16.
+        clear r; set (r := if _ <? _ then Some (Hexadecimal _ _) else Some _).
+        clear m; set (m := match nb_digits f with 0 => _ | _ => _ end).
+        replace m with r; [unfold r|now unfold m; revert Hf; case f].
+        rewrite HexadecimalZ.to_of, abs_norm, abs_app_int.
+        case Nat.ltb_spec; intro Hnf.
+        -- rewrite (del_tail_app_int_exact _ _ Hnf).
+           rewrite (del_head_app_int_exact _ _ Hnf).
+           now rewrite (dnorm_i_exact _ _ Hnf).
+        -- rewrite (unorm_app_r _ _ Hnf).
+           rewrite (iter_D0_unorm _ Hf).
+           now rewrite dnorm_i_exact'.
+    + set (i' := match i with Pos _ => _ | _ => _ end).
+      set (m := match Pos.to_uint e with Decimal.Nil => _ | _ => _ end).
+      replace m with (HexadecimalExp i' f (Decimal.Pos (Pos.to_uint e))).
+      2:{ unfold m; generalize (DecimalPos.Unsigned.to_uint_nonzero e).
+          now case Pos.to_uint; [|intro u; case u|..]. }
+      unfold i'; clear i' m.
+      case (uint_eq_dec f Nil); intro Hf.
+      * rewrite Hf; clear f Hf.
+        unfold to_hexadecimal; simpl.
+        rewrite IZ_to_Z_IZ_of_Z, HexadecimalZ.to_of.
+        case i as [i|i]; [now simpl|]; simpl.
+        rewrite app_nil_r.
+        case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi].
+        now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead.
+      * set (r := IRQ _).
+        set (m := match f with Nil => _ | _ => _ end).
+        replace m with r; [unfold r|now unfold m; revert Hf; case f].
+        unfold to_hexadecimal; simpl.
+        unfold IQmake_to_hexadecimal; simpl.
+        set (n := Nat.iter _ _ _).
+        case (Pos.eq_dec n 1); intro Hn.
+        exfalso; apply Hf.
+        { now apply nb_digits_0; revert Hn; unfold n; case nb_digits. }
+        clear m; set (m := match n with 1%positive | _ => _ end).
+        replace m with (QArith_base.IQmake_to_hexadecimal (Z.of_hex_int (app_int i f)) n).
+        2:{ now unfold m; revert Hn; case n. }
+        unfold QArith_base.IQmake_to_hexadecimal, n; simpl.
+        rewrite nztail_to_hex_uint_pow16.
+        clear r; set (r := if _ <? _ then Some (Hexadecimal _ _) else Some _).
+        clear m; set (m := match nb_digits f with 0 => _ | _ => _ end).
+        replace m with r; [unfold r|now unfold m; revert Hf; case f].
+        rewrite HexadecimalZ.to_of, abs_norm, abs_app_int.
+        case Nat.ltb_spec; intro Hnf.
+        -- rewrite (del_tail_app_int_exact _ _ Hnf).
+           rewrite (del_head_app_int_exact _ _ Hnf).
+           now rewrite (dnorm_i_exact _ _ Hnf).
+        -- rewrite (unorm_app_r _ _ Hnf).
+           rewrite (iter_D0_unorm _ Hf).
+           now rewrite dnorm_i_exact'.
+    + case (uint_eq_dec f Nil); intro Hf.
+      * rewrite Hf; clear f Hf.
+        unfold to_hexadecimal; simpl.
+        rewrite IZ_to_Z_IZ_of_Z, HexadecimalZ.to_of.
+        case i as [i|i]; [now simpl|]; simpl.
+        rewrite app_nil_r.
+        case (uint_eq_dec (nzhead i) Nil); [now intros->|intro Hi].
+        now rewrite (unorm_nzhead _ Hi); revert Hi; case nzhead.
+      * set (r := IRQ _).
+        set (m := match f with Nil => _ | _ => _ end).
+        replace m with r; [unfold r|now unfold m; revert Hf; case f].
+        unfold to_hexadecimal; simpl.
+        unfold IQmake_to_hexadecimal; simpl.
+        set (n := Nat.iter _ _ _).
+        case (Pos.eq_dec n 1); intro Hn.
+        exfalso; apply Hf.
+        { now apply nb_digits_0; revert Hn; unfold n; case nb_digits. }
+        clear m; set (m := match n with 1%positive | _ => _ end).
+        replace m with (QArith_base.IQmake_to_hexadecimal (Z.of_hex_int (app_int i f)) n).
+        2:{ now unfold m; revert Hn; case n. }
+        unfold QArith_base.IQmake_to_hexadecimal, n; simpl.
+        rewrite nztail_to_hex_uint_pow16.
+        clear r; set (r := if _ <? _ then Some (Hexadecimal _ _) else Some _).
+        clear m; set (m := match nb_digits f with 0 => _ | _ => _ end).
+        replace m with r; [unfold r|now unfold m; revert Hf; case f].
+        rewrite HexadecimalZ.to_of, abs_norm, abs_app_int.
+        case Nat.ltb_spec; intro Hnf.
+        -- rewrite (del_tail_app_int_exact _ _ Hnf).
+           rewrite (del_head_app_int_exact _ _ Hnf).
+           now rewrite (dnorm_i_exact _ _ Hnf).
+        -- rewrite (unorm_app_r _ _ Hnf).
+           rewrite (iter_D0_unorm _ Hf).
+           now rewrite dnorm_i_exact'.
+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 (dnorm d).
+Proof.
+  exists (of_hexadecimal d). apply to_of.
+Qed.
+
+Lemma of_hexadecimal_dnorm d : of_hexadecimal (dnorm d) = of_hexadecimal d.
+Proof. now apply to_hexadecimal_inj; rewrite !to_of; [|rewrite dnorm_involutive]. Qed.
+
+Lemma of_inj d d' : of_hexadecimal d = of_hexadecimal d' -> dnorm d = dnorm d'.
+Proof.
+  intro H.
+  apply (@f_equal _ _ (fun x => match x with Some x => x | _ => d end)
+                  (Some (dnorm d)) (Some (dnorm d'))).
+  now rewrite <- !to_of, H.
+Qed.
+
+Lemma of_iff d d' : of_hexadecimal d = of_hexadecimal d' <-> dnorm d = dnorm d'.
+Proof.
+  split. apply of_inj. intros E. rewrite <- of_hexadecimal_dnorm, E.
+  apply of_hexadecimal_dnorm.
+Qed.
diff --git a/theories/Numbers/HexadecimalZ.v b/theories/Numbers/HexadecimalZ.v
index c5ed0b5b28..1d78ad1ad2 100644
--- a/theories/Numbers/HexadecimalZ.v
+++ b/theories/Numbers/HexadecimalZ.v
@@ -80,9 +80,11 @@ 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 <-(rev_rev (app _ _)), <-(of_list_to_list (rev (app _ _))).
+  rewrite rev_spec, app_spec, List.rev_app_distr.
+  rewrite <-!rev_spec, <-app_spec, of_list_to_list.
+  unfold Z.of_hex_uint; rewrite Unsigned.of_lu_rev.
+  unfold app; rewrite Unsigned.of_lu_revapp, !rev_rev.
   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]. }
@@ -140,3 +142,22 @@ 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.
+
+Lemma nztail_to_hex_uint_pow16 n :
+  Hexadecimal.nztail (Pos.to_hex_uint (Nat.iter n (Pos.mul 16) 1%positive))
+  = (D1 Nil, n).
+Proof.
+  case n as [|n]; [now simpl|].
+  rewrite <-(Nat2Pos.id (S n)); [|now simpl].
+  generalize (Pos.of_nat (S n)); clear n; intro p.
+  induction (Pos.to_nat p); [now simpl|].
+  rewrite Unsigned.nat_iter_S.
+  unfold Pos.to_hex_uint.
+  change (Pos.to_little_hex_uint _)
+    with (Unsigned.to_lu (16 * N.pos (Nat.iter n (Pos.mul 16) 1%positive))).
+  rewrite Unsigned.to_lhex_tenfold.
+  revert IHn; unfold Pos.to_hex_uint.
+  unfold Hexadecimal.nztail; rewrite !rev_rev; simpl.
+  set (f'' := _ (Pos.to_little_hex_uint _)).
+  now case f''; intros r n' H; inversion H.
+Qed.