[numeral notation] Prove Q

10 files changed, 1742 insertions, 351 deletions

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 d9642d7b02..2027813eec 100644
--- a/theories/Numbers/DecimalQ.v
+++ b/theories/Numbers/DecimalQ.v
@@ -15,8 +15,112 @@
 
 Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith.
 
+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.
+  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.
+
+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.
-Admitted.
+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.
 
 Definition dnorm (d:decimal) : decimal :=
   let norm_i i f :=
@@ -43,13 +147,50 @@ Lemma dnorm_spec_i d :
     (i' = Neg (unorm i) /\ (nzhead i <> Nil \/ nzhead f <> Nil))
     \/ (i' = Pos zero /\ (nzhead i = Nil /\ nzhead f = Nil))
   end.
-Admitted.
+Proof.
+  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.
-Admitted.
+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 dnorm_spec_e d :
   match d, dnorm d with
@@ -58,24 +199,241 @@ Lemma dnorm_spec_e d :
     | DecimalExp _ _ e, DecimalExp _ _ e' => e' = norm e /\ e' <> Pos zero
     | Decimal _ _, DecimalExp _ _ _ => False
   end.
-Admitted.
+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 dnorm_invol d : dnorm (dnorm d) = dnorm d.
-Admitted.
+Lemma dnorm_involutive d : dnorm (dnorm d) = dnorm d.
+Proof.
+  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 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:decimal) : to_decimal (of_decimal d) = Some (dnorm d).
-Admitted.
+Proof.
+  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 *)
 
 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).
+  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).
@@ -84,18 +442,18 @@ Proof.
 Qed.
 
 Lemma of_decimal_dnorm d : of_decimal (dnorm d) = of_decimal d.
-Proof. now apply to_decimal_inj; rewrite !to_of; [|rewrite dnorm_invol]. Qed.
+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.
+  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.
+  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 bbafa7ddc1..a32019767c 100644
--- a/theories/Numbers/HexadecimalQ.v
+++ b/theories/Numbers/HexadecimalQ.v
@@ -16,8 +16,109 @@
 Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ.
 Require Import Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN HexadecimalZ QArith.
 
+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.
-Admitted.
+Proof.
+  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.
+
 
 Definition dnorm (d:hexadecimal) : hexadecimal :=
   let norm_i i f :=
@@ -44,13 +145,50 @@ Lemma dnorm_spec_i d :
     (i' = Neg (unorm i) /\ (nzhead i <> Nil \/ nzhead f <> Nil))
     \/ (i' = Pos zero /\ (nzhead i = Nil /\ nzhead f = Nil))
   end.
-Admitted.
+Proof.
+  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 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.
-Admitted.
+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
@@ -61,24 +199,241 @@ Lemma dnorm_spec_e d :
       e' = Decimal.norm e /\ e' <> Decimal.Pos Decimal.zero
     | Hexadecimal _ _, HexadecimalExp _ _ _ => False
   end.
-Admitted.
+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_invol d : dnorm (dnorm d) = dnorm d.
-Admitted.
+Lemma dnorm_involutive d : dnorm (dnorm d) = dnorm d.
+Proof.
+  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).
-Admitted.
+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 *)
 
 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).
+  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).
@@ -87,18 +442,18 @@ Proof.
 Qed.
 
 Lemma of_hexadecimal_dnorm d : of_hexadecimal (dnorm d) = of_hexadecimal d.
-Proof. now apply to_hexadecimal_inj; rewrite !to_of; [|rewrite dnorm_invol]. Qed.
+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.
+  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.
+  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.