Decimal: prove numeral notation for Q

Fill in the proofs, adding a few neessary lemmas along the way.

5 files changed, 842 insertions, 14 deletions

diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 2a84456500..5eae5567d7 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -16,7 +16,7 @@
     We represent numbers in base 10 as lists of decimal digits,
     in big-endian order (most significant digit comes first). *)
 
-Require Import Datatypes.
+Require Import Datatypes Specif.
 
 (** Unsigned integers are just lists of digits.
     For instance, ten is (D1 (D0 Nil)) *)
@@ -53,6 +53,10 @@ Variant decimal :=
  | Decimal (i:int) (f:uint)
  | DecimalExp (i:int) (f:uint) (e:int).
 
+Scheme Equality for uint.
+Scheme Equality for int.
+Scheme Equality for decimal.
+
 Declare Scope dec_uint_scope.
 Delimit Scope dec_uint_scope with uint.
 Bind Scope dec_uint_scope with uint.
@@ -172,8 +176,8 @@ Fixpoint del_head n d :=
 
 Definition del_head_int n d :=
   match d with
-  | Pos d => Pos (del_head n d)
-  | Neg d => Neg (del_head n d)
+  | Pos d => del_head n d
+  | Neg d => del_head n d
   end.
 
 (** [del_tail n d] removes [n] digits at end of [d]
diff --git a/theories/Numbers/DecimalFacts.v b/theories/Numbers/DecimalFacts.v
index 1bf24099e4..dd361562ba 100644
--- a/theories/Numbers/DecimalFacts.v
+++ b/theories/Numbers/DecimalFacts.v
@@ -10,7 +10,7 @@
 
 (** * DecimalFacts : some facts about Decimal numbers *)
 
-Require Import Decimal.
+Require Import Decimal Arith.
 
 Lemma uint_dec (d d' : uint) : { d = d' } + { d <> d' }.
 Proof.
@@ -28,6 +28,157 @@ Proof.
   apply rev_revapp.
 Qed.
 
+Lemma revapp_rev_nil d : revapp (rev d) Nil = d.
+Proof. now fold (rev (rev d)); rewrite rev_rev. Qed.
+
+Lemma app_nil_r d : app d Nil = d.
+Proof. now unfold app; rewrite revapp_rev_nil. Qed.
+
+Lemma app_int_nil_r d : app_int d Nil = d.
+Proof. now case d; intro d'; simpl; rewrite app_nil_r. Qed.
+
+Lemma revapp_revapp_1 d d' d'' :
+  nb_digits d <= 1 ->
+  revapp (revapp d d') d'' = revapp d' (revapp d d'').
+Proof.
+  now case d; clear d; intro d;
+    [|case d; clear d; intro d;
+      [|simpl; case nb_digits; [|intros n]; intros Hn; exfalso;
+        [apply (Nat.nle_succ_diag_l _ Hn)|
+         apply (Nat.nle_succ_0 _ (le_S_n _ _ Hn))]..]..].
+Qed.
+
+Lemma nb_digits_pos d : d <> Nil -> 0 < nb_digits d.
+Proof. now case d; [|intros d' _; apply Nat.lt_0_succ..]. Qed.
+
+Lemma nb_digits_revapp d d' :
+  nb_digits (revapp d d') = nb_digits d + nb_digits d'.
+Proof.
+  now revert d'; induction d; [|intro d'; simpl; rewrite IHd; simpl..].
+Qed.
+
+Lemma nb_digits_rev u : nb_digits (rev u) = nb_digits u.
+Proof. now unfold rev; rewrite nb_digits_revapp. Qed.
+
+Lemma nb_digits_nzhead u : nb_digits (nzhead u) <= nb_digits u.
+Proof. now induction u; [|apply le_S|..]. Qed.
+
+Lemma del_head_nb_digits (u:uint) : del_head (nb_digits u) u = Nil.
+Proof. now induction u. Qed.
+
+Lemma nb_digits_del_head n u :
+  n <= nb_digits u -> nb_digits (del_head n u) = nb_digits u - n.
+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..].
+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 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 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)).
+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.
+Proof. now case d; clear d; simpl; intros u Hu; rewrite app_del_tail_head. Qed.
+
 (** Normalization on little-endian numbers *)
 
 Fixpoint nztail d :=
@@ -83,6 +234,12 @@ Proof.
   - now rewrite <- nzhead_rev, rev_rev.
 Qed.
 
+Lemma nzhead_D0 u : nzhead (D0 u) = nzhead u.
+Proof. reflexivity. Qed.
+
+Lemma nzhead_iter_D0 n u : nzhead (Nat.iter n D0 u) = nzhead u.
+Proof. now induction n. Qed.
+
 Lemma revapp_nil_inv d d' : revapp d d' = Nil -> d = Nil /\ d' = Nil.
 Proof.
   revert d'.
@@ -121,11 +278,50 @@ 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.
+  now revert n; induction u; intro n;
+    [|case n; [|intro n'; simpl; intro H; apply IHu, lt_S_n]..].
+Qed.
+
+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_invol d : nzhead (nzhead d) = nzhead d.
 Proof.
   now induction d.
 Qed.
 
+Lemma nztail_invol d : nztail (nztail d) = nztail d.
+Proof.
+  rewrite <-(rev_rev (nztail _)), <-(rev_rev (nztail d)), <-(rev_rev d).
+  now rewrite !rev_nztail_rev, nzhead_invol.
+Qed.
+
 Lemma unorm_invol d : unorm (unorm d) = unorm d.
 Proof.
   unfold unorm.
@@ -141,3 +337,123 @@ Proof.
   - destruct (nzhead d) eqn:E; auto.
     destruct (nzhead_nonzero _ _ E).
 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.
+  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'.
+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.
+
+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).
+  - 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_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').
+Proof.
+  unfold app.
+  rewrite <-(rev_nztail_rev d), rev_rev.
+  generalize (rev d); clear d; intro d.
+  generalize (nzhead_revapp_0 d d').
+  generalize (nzhead_revapp d d').
+  generalize (nzhead_revapp_0 (nztail d) d').
+  generalize (nzhead_revapp (nztail d) d').
+  rewrite nztail_invol.
+  now case nztail;
+    [intros _ H _ H'; rewrite (H eq_refl), (H' eq_refl)
+    |intros d'' H _ H' _; rewrite H; [rewrite H'|]..].
+Qed.
+
+Lemma unorm_app_unorm d d' :
+  unorm (app (unorm d) d') = unorm (app d d').
+Proof.
+  unfold unorm.
+  rewrite <-(nzhead_app_nzhead d d').
+  now case (nzhead d).
+Qed.
+
+Lemma norm_app_int_norm d d' :
+  unorm d' = zero ->
+  norm (app_int (norm d) d') = norm (app_int d d').
+Proof.
+  case d; clear d; intro d; simpl.
+  - now rewrite unorm_app_unorm.
+  - unfold app_int, app.
+    rewrite unorm_0; intro Hd'.
+    rewrite <-rev_nztail_rev.
+    generalize (nzhead_revapp (rev d) d').
+    generalize (nzhead_revapp_0 (rev d) d').
+    now case_eq (nztail (rev d));
+      [intros Hd'' H _; rewrite (H eq_refl); simpl;
+       unfold unorm; simpl; rewrite Hd'
+      |intros d'' Hd'' _ H; rewrite H; clear H; [|now simpl];
+       set (r := rev _);
+       set (m := match r with Nil => Pos zero | _ => _ end);
+       assert (H' : m = Neg r);
+       [now unfold m; case_eq r; unfold r;
+        [intro H''; generalize (rev_nil_inv _ H'')|..]
+       |rewrite H'; unfold r; clear m r H'];
+       unfold norm;
+       rewrite rev_rev, <-Hd'';
+       rewrite nzhead_revapp; rewrite nztail_invol; [|rewrite Hd'']..].
+Qed.
diff --git a/theories/Numbers/DecimalPos.v b/theories/Numbers/DecimalPos.v
index 4ec610faa2..5611329b12 100644
--- a/theories/Numbers/DecimalPos.v
+++ b/theories/Numbers/DecimalPos.v
@@ -325,6 +325,21 @@ Proof.
   apply of_uint_norm.
 Qed.
 
+Lemma nztail_to_uint p :
+  let (h, n) := Decimal.nztail (Pos.to_uint p) in
+  Npos p = Pos.of_uint h * 10^(N.of_nat n).
+Proof.
+  rewrite <-(of_to p), <-(rev_rev (Pos.to_uint p)), of_lu_rev.
+  unfold Decimal.nztail.
+  rewrite rev_rev.
+  induction (rev (Pos.to_uint p)); [reflexivity| |
+    now simpl N.of_nat; simpl N.pow; rewrite N.mul_1_r, of_lu_rev..].
+  revert IHu.
+  set (t := _ u); case t; clear t; intros u0 n H.
+  rewrite of_lu_eqn; unfold hd, tl.
+  rewrite N.add_0_l, H, Nat2N.inj_succ, N.pow_succ_r'; ring.
+Qed.
+
 End Unsigned.
 
 (** Conversion from/to signed decimal numbers *)
diff --git a/theories/Numbers/DecimalQ.v b/theories/Numbers/DecimalQ.v
index d2cd061594..c51cced024 100644
--- a/theories/Numbers/DecimalQ.v
+++ b/theories/Numbers/DecimalQ.v
@@ -16,7 +16,62 @@
 Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith.
 
 Lemma of_to (q:Q) : forall d, to_decimal q = Some d -> of_decimal d = q.
-Admitted.
+Proof.
+  cut (match to_decimal q with None => True | Some d => of_decimal d = q end).
+  { now case to_decimal; [intros d <- d' Hd'; injection Hd'; intros ->|]. }
+  destruct q as (num, den).
+  unfold to_decimal; simpl.
+  generalize (DecimalPos.Unsigned.nztail_to_uint den).
+  case Decimal.nztail; intros u n.
+  case u; clear u; [intros; exact I|intros; exact I|intro u|intros; exact I..].
+  case u; clear u; [|intros; exact I..].
+  unfold Pos.of_uint, Pos.of_uint_acc; rewrite N.mul_1_l.
+  case n.
+  - unfold of_decimal, app_int, app, Z.to_int; simpl.
+    intro H; inversion H as (H1); clear H H1.
+    case num; [reflexivity|intro pnum; fold (rev (rev (Pos.to_uint pnum)))..].
+    + rewrite rev_rev; simpl.
+      now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to.
+    + rewrite rev_rev; simpl.
+      now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to.
+  - clear n; intros n H.
+    injection H; clear H; intros ->.
+    case Nat.ltb.
+    + unfold of_decimal.
+      rewrite of_to.
+      apply f_equal2; [|now simpl].
+      unfold app_int, app, Z.to_int; simpl.
+      now case num;
+        [|intro pnum; fold (rev (rev (Pos.to_uint pnum)));
+          rewrite rev_rev; unfold Z.of_int, Z.of_uint;
+          rewrite DecimalPos.Unsigned.of_to..].
+    + unfold of_decimal; case Nat.ltb_spec; intro Hn; simpl.
+      * rewrite nb_digits_del_head; [|now apply Nat.le_sub_l].
+        rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l].
+        rewrite Nat2Z.inj_sub; [|now apply le_Sn_le].
+        rewrite Z.sub_sub_distr, Z.sub_diag; simpl.
+        rewrite <-(of_to num) at 4.
+        now revert Hn; case Z.to_int; clear num; intros pnum Hn; simpl;
+          (rewrite app_del_tail_head; [|now apply le_Sn_le]).
+      * revert Hn.
+        set (anum := match Z.to_int num with Pos i => i | _ => _ end).
+        intro Hn.
+        assert (H : exists l, nb_digits anum = S l).
+        { exists (Nat.pred (nb_digits anum)); apply S_pred_pos.
+          now unfold anum; case num;
+            [apply Nat.lt_0_1|
+             intro pnum; apply nb_digits_pos, Unsigned.to_uint_nonnil..]. }
+        destruct H as (l, Hl); rewrite Hl.
+        assert (H : forall n d, (nb_digits (Nat.iter n D0 d) = n + nb_digits d)%nat).
+        { now intros n'; induction n'; intro d; [|simpl; rewrite IHn']. }
+        rewrite H, Hl.
+        rewrite Nat.add_succ_r, Nat.sub_add; [|now apply le_S_n; rewrite <-Hl].
+        assert (H' : forall n d, Pos.of_uint (Nat.iter n D0 d) = Pos.of_uint d).
+        { now intro n'; induction n'; intro d; [|simpl; rewrite IHn']. }
+        now unfold anum; case num; simpl; [|intro pnum..];
+          unfold app, Z.of_uint; simpl;
+            rewrite H', ?DecimalPos.Unsigned.of_to.
+Qed.
 
 (* normalize without fractional part, for instance norme 12.3e-1 is 123e-2 *)
 Definition dnorme (d:decimal) : decimal :=
@@ -58,38 +113,449 @@ Lemma dnorme_spec d :
   | DecimalExp i Nil e => i = norm i /\ e = norm e /\ e <> Pos zero
   | _ => False
   end.
-Admitted.
+Proof.
+  case d; clear d; intros i f; [|intro e]; unfold dnorme; simpl.
+  - set (e' := Z.to_int _).
+    case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne'].
+    + now rewrite norm_invol.
+    + set (r := DecimalExp _ _ _).
+      set (m := match norm e' with Pos zero => _ | _ => _ end).
+      replace m with r; [now unfold r; rewrite !norm_invol|].
+      unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
+      now case e''; [|intro e'''; case e'''..].
+  - set (e' := Z.to_int _).
+    case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne'].
+    + now rewrite norm_invol.
+    + set (r := DecimalExp _ _ _).
+      set (m := match norm e' with Pos zero => _ | _ => _ end).
+      replace m with r; [now unfold r; rewrite !norm_invol|].
+      unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
+      now case e''; [|intro e'''; case e'''..].
+Qed.
 
 Lemma dnormf_spec d :
   match dnormf d with
   | Decimal i f => i = Neg zero \/ i = norm i
   | _ => False
   end.
-Admitted.
+Proof.
+  case d; clear d; intros i f; [|intro e]; unfold dnormf, dnorme; simpl.
+  - set (e' := Z.to_int _).
+    case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne'].
+    + now right; rewrite norm_invol.
+    + set (r := DecimalExp _ _ _).
+      set (m := match norm e' with Pos zero => _ | _ => _ end).
+      assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
+      { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
+        now case e''; [|intro e'''; case e'''..]. }
+      rewrite <-DecimalZ.to_of, DecimalZ.of_to.
+      case_eq (Z.of_int e'); [|intros pe'..]; intro Hpe';
+        [now right; rewrite norm_invol..|].
+      case Nat.ltb_spec.
+      * now intro H; rewrite (norm_del_tail_int_norm _ _ H); right.
+      * now intros _; case norm; intros _; [right|left].
+  - set (e' := Z.to_int _).
+    case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne'].
+    + now right; rewrite norm_invol.
+    + set (r := DecimalExp _ _ _).
+      set (m := match norm e' with Pos zero => _ | _ => _ end).
+      assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
+      { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
+        now case e''; [|intro e'''; case e'''..]. }
+      rewrite <-DecimalZ.to_of, DecimalZ.of_to.
+      case_eq (Z.of_int e'); [|intros pe'..]; intro Hpe';
+        [now right; rewrite norm_invol..|].
+      case Nat.ltb_spec.
+      * now intro H; rewrite (norm_del_tail_int_norm _ _ H); right.
+      * now intros _; case norm; intros _; [right|left].
+Qed.
 
 Lemma dnorme_invol d : dnorme (dnorme d) = dnorme d.
-Admitted.
+Proof.
+  case d; clear d; intros i f; [|intro e]; unfold dnorme; simpl.
+  - set (e' := Z.to_int _).
+    case (int_eq_dec (norm e') (Pos zero)); intro Hne'.
+    + rewrite Hne'; simpl; rewrite app_int_nil_r, norm_invol.
+      revert Hne'.
+      rewrite <-to_of.
+      change (Pos zero) with (Z.to_int 0).
+      intro H; generalize (to_int_inj _ _ H); clear H.
+      unfold e'; rewrite DecimalZ.of_to.
+      now case f; [rewrite app_int_nil_r|..].
+    + set (r := DecimalExp _ _ _).
+      set (m := match norm e' with Pos zero => _ | _ => _ end).
+      assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
+      { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
+        now case e''; [|intro e'''; case e'''..]. }
+      rewrite <-DecimalZ.to_of, DecimalZ.of_to.
+      unfold nb_digits, Z.of_nat; rewrite Z.sub_0_r, to_of, norm_invol.
+      rewrite app_int_nil_r, norm_invol.
+      set (r := DecimalExp _ _ _).
+      set (m := match norm e' with Pos zero => _ | _ => _ end).
+      unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
+      now case e''; [|intro e'''; case e'''..].
+  - set (e' := Z.to_int _).
+    case (int_eq_dec (norm e') (Pos zero)); intro Hne'.
+    + rewrite Hne'; simpl; rewrite app_int_nil_r, norm_invol.
+      revert Hne'.
+      rewrite <-to_of.
+      change (Pos zero) with (Z.to_int 0).
+      intro H; generalize (to_int_inj _ _ H); clear H.
+      unfold e'; rewrite DecimalZ.of_to.
+      now case f; [rewrite app_int_nil_r|..].
+    + set (r := DecimalExp _ _ _).
+      set (m := match norm e' with Pos zero => _ | _ => _ end).
+      assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
+      { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
+        now case e''; [|intro e'''; case e'''..]. }
+      rewrite <-DecimalZ.to_of, DecimalZ.of_to.
+      unfold nb_digits, Z.of_nat; rewrite Z.sub_0_r, to_of, norm_invol.
+      rewrite app_int_nil_r, norm_invol.
+      set (r := DecimalExp _ _ _).
+      set (m := match norm e' with Pos zero => _ | _ => _ end).
+      unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
+      now case e''; [|intro e'''; case e'''..].
+Qed.
 
 Lemma dnormf_invol d : dnormf (dnormf d) = dnormf d.
-Admitted.
+Proof.
+  case d; clear d; intros i f; [|intro e]; unfold dnormf, dnorme; simpl.
+  - set (e' := Z.to_int _).
+    case (int_eq_dec (norm e') (Pos zero)); intro Hne'.
+    + rewrite Hne'; simpl; rewrite app_int_nil_r, norm_invol.
+      revert Hne'.
+      rewrite <-to_of.
+      change (Pos zero) with (Z.to_int 0).
+      intro H; generalize (to_int_inj _ _ H); clear H.
+      unfold e'; rewrite DecimalZ.of_to.
+      now case f; [rewrite app_int_nil_r|..].
+    + set (r := DecimalExp _ _ _).
+      set (m := match norm e' with Pos zero => _ | _ => _ end).
+      assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
+      { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
+        now case e''; [|intro e'''; case e'''..]. }
+      rewrite of_int_norm.
+      case_eq (Z.of_int e'); [|intro pe'..]; intro Hnpe';
+        [now simpl; rewrite app_int_nil_r, norm_invol..|].
+      case Nat.ltb_spec; intro Hpe'.
+      * rewrite nb_digits_del_head; [|now apply Nat.le_sub_l].
+        rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l].
+        rewrite Nat2Z.inj_sub; [|now apply Nat.lt_le_incl].
+        simpl.
+        rewrite Z.sub_sub_distr, Z.sub_diag, Z.add_0_l.
+        rewrite <-DecimalZ.to_of, DecimalZ.of_to.
+        rewrite positive_nat_Z; simpl.
+        unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
+        rewrite app_int_del_tail_head; [|now apply Nat.lt_le_incl].
+        now rewrite norm_invol, (proj2 (Nat.ltb_lt _ _) Hpe').
+      * simpl.
+        rewrite nb_digits_iter_D0.
+        rewrite (Nat.sub_add _ _ Hpe').
+        rewrite <-DecimalZ.to_of, DecimalZ.of_to.
+        rewrite positive_nat_Z; simpl.
+        unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
+        revert Hpe'.
+        set (i' := norm (app_int i f)).
+        case_eq i'; intros u Hu Hpe'.
+        ++ simpl; unfold app; simpl.
+           rewrite unorm_D0, unorm_iter_D0.
+           assert (Hu' : unorm u = u).
+           { generalize (f_equal norm Hu).
+             unfold i'; rewrite norm_invol; fold i'.
+             now simpl; rewrite Hu; intro H; injection H. }
+           now rewrite Hu', (proj2 (Nat.ltb_ge _ _) Hpe').
+        ++ simpl; rewrite nzhead_iter_D0.
+           assert (Hu' : nzhead u = u).
+           { generalize (f_equal norm Hu).
+             unfold i'; rewrite norm_invol; fold i'.
+             now rewrite Hu; simpl; case (nzhead u); [|intros u' H; injection H..]. }
+           rewrite Hu'.
+           assert (Hu'' : u <> Nil).
+           { intro H; revert Hu; rewrite H; unfold i'.
+             now case app_int; intro u'; [|simpl; case nzhead]. }
+           set (m := match u with Nil => Pos zero | _ => _ end).
+           assert (H : m = Neg u); [|rewrite H; clear m H].
+           { now revert Hu''; unfold m; case u. }
+           now rewrite (proj2 (Nat.ltb_ge _ _) Hpe').
+  - set (e' := Z.to_int _).
+    case (int_eq_dec (norm e') (Pos zero)); intro Hne'.
+    + rewrite Hne'; simpl; rewrite app_int_nil_r, norm_invol.
+      revert Hne'.
+      rewrite <-to_of.
+      change (Pos zero) with (Z.to_int 0).
+      intro H; generalize (to_int_inj _ _ H); clear H.
+      unfold e'; rewrite DecimalZ.of_to.
+      now case f; [rewrite app_int_nil_r|..].
+    + set (r := DecimalExp _ _ _).
+      set (m := match norm e' with Pos zero => _ | _ => _ end).
+      assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
+      { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
+        now case e''; [|intro e'''; case e'''..]. }
+      rewrite of_int_norm.
+      case_eq (Z.of_int e'); [|intro pe'..]; intro Hnpe';
+        [now simpl; rewrite app_int_nil_r, norm_invol..|].
+      case Nat.ltb_spec; intro Hpe'.
+      * rewrite nb_digits_del_head; [|now apply Nat.le_sub_l].
+        rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l].
+        rewrite Nat2Z.inj_sub; [|now apply Nat.lt_le_incl].
+        simpl.
+        rewrite Z.sub_sub_distr, Z.sub_diag, Z.add_0_l.
+        rewrite <-DecimalZ.to_of, DecimalZ.of_to.
+        rewrite positive_nat_Z; simpl.
+        unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
+        rewrite app_int_del_tail_head; [|now apply Nat.lt_le_incl].
+        now rewrite norm_invol, (proj2 (Nat.ltb_lt _ _) Hpe').
+      * simpl.
+        rewrite nb_digits_iter_D0.
+        rewrite (Nat.sub_add _ _ Hpe').
+        rewrite <-DecimalZ.to_of, DecimalZ.of_to.
+        rewrite positive_nat_Z; simpl.
+        unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
+        revert Hpe'.
+        set (i' := norm (app_int i f)).
+        case_eq i'; intros u Hu Hpe'.
+        ++ simpl; unfold app; simpl.
+           rewrite unorm_D0, unorm_iter_D0.
+           assert (Hu' : unorm u = u).
+           { generalize (f_equal norm Hu).
+             unfold i'; rewrite norm_invol; fold i'.
+             now simpl; rewrite Hu; intro H; injection H. }
+           now rewrite Hu', (proj2 (Nat.ltb_ge _ _) Hpe').
+        ++ simpl; rewrite nzhead_iter_D0.
+           assert (Hu' : nzhead u = u).
+           { generalize (f_equal norm Hu).
+             unfold i'; rewrite norm_invol; fold i'.
+             now rewrite Hu; simpl; case (nzhead u); [|intros u' H; injection H..]. }
+           rewrite Hu'.
+           assert (Hu'' : u <> Nil).
+           { intro H; revert Hu; rewrite H; unfold i'.
+             now case app_int; intro u'; [|simpl; case nzhead]. }
+           set (m := match u with Nil => Pos zero | _ => _ end).
+           assert (H : m = Neg u); [|rewrite H; clear m H].
+           { now revert Hu''; unfold m; case u. }
+           now rewrite (proj2 (Nat.ltb_ge _ _) Hpe').
+Qed.
 
 Lemma to_of (d:decimal) :
   to_decimal (of_decimal d) = Some (dnorme d)
   \/ to_decimal (of_decimal d) = Some (dnormf d).
-Admitted.
+Proof.
+  unfold to_decimal.
+  pose (t10 := fun y => ((y + y~0~0)~0)%positive).
+  assert (H : exists e_den,
+             Decimal.nztail (Pos.to_uint (Qden (of_decimal d))) = (D1 Nil, e_den)).
+  { assert (H : forall p,
+               Decimal.nztail (Pos.to_uint (Pos.iter t10 1%positive p))
+               = (D1 Nil, Pos.to_nat p)).
+    { intro p; rewrite Pos2Nat.inj_iter.
+      fold (Nat.iter (Pos.to_nat p) t10 1%positive).
+      induction (Pos.to_nat p); [now simpl|].
+      rewrite DecimalPos.Unsigned.nat_iter_S.
+      unfold Pos.to_uint.
+      change (Pos.to_little_uint _)
+        with (Unsigned.to_lu (10 * N.pos (Nat.iter n t10 1%positive))).
+      rewrite Unsigned.to_ldec_tenfold.
+      revert IHn; unfold Pos.to_uint.
+      unfold Decimal.nztail; rewrite !rev_rev; simpl.
+      set (f'' := _ (Pos.to_little_uint _)).
+      now case f''; intros r n' H; inversion H. }
+    case d; intros i f; [|intro e]; unfold of_decimal; simpl.
+    - case (- Z.of_nat _)%Z; [|intro p..]; simpl; [now exists O..|].
+      exists (Pos.to_nat p); apply H.
+    - case (_ - _)%Z; [|intros p..]; simpl; [now exists O..|].
+      exists (Pos.to_nat p); apply H. }
+  generalize (DecimalPos.Unsigned.nztail_to_uint (Qden (of_decimal d))).
+  destruct H as (e, He); rewrite He; clear He; simpl.
+  assert (Hn1 : forall p, N.pos (Pos.iter t10 1%positive p) = 1%N -> False).
+  { intro p.
+    rewrite Pos2Nat.inj_iter.
+    case_eq (Pos.to_nat p); [|now simpl].
+    intro H; exfalso; apply (lt_irrefl O).
+    rewrite <-H at 2; apply Pos2Nat.is_pos. }
+  assert (Ht10inj : forall n m, t10 n = t10 m -> n = m).
+  { intros n m H; generalize (f_equal Z.pos H); clear H.
+    change (Z.pos (t10 n)) with (Z.mul 10 (Z.pos n)).
+    change (Z.pos (t10 m)) with (Z.mul 10 (Z.pos m)).
+    rewrite Z.mul_comm, (Z.mul_comm 10).
+    intro H; generalize (f_equal (fun z => Z.div z 10) H); clear H.
+    now rewrite !Z.div_mul; [|now simpl..]; intro H; inversion H. }
+  assert (Hinj : forall n m,
+             Nat.iter n t10 1%positive = Nat.iter m t10 1%positive -> n = m).
+  { induction n; [now intro m; case m|].
+    intro m; case m; [now simpl|]; clear m; intro m.
+    rewrite !Unsigned.nat_iter_S.
+    intro H; generalize (Ht10inj _ _ H); clear H; intro H.
+    now rewrite (IHn _ H). }
+  case e; clear e; [|intro e]; simpl; unfold of_decimal, dnormf, dnorme.
+  - case d; clear d; intros i f; [|intro e]; simpl.
+    + intro H; left; revert H.
+      generalize (nb_digits_pos f).
+      case f;
+        [|now clear f; intro f; intros H1 H2; exfalso; revert H1 H2;
+          case nb_digits; simpl;
+          [intros H _; apply (lt_irrefl O), H|intros n _; apply Hn1]..].
+      now intros _ _; simpl; rewrite to_of.
+    + intro H; right; revert H.
+      rewrite <-to_of, DecimalZ.of_to.
+      set (emf := (_ - _)%Z).
+      case_eq emf; [|intro pemf..].
+      * now simpl; rewrite to_of.
+      * set (r := DecimalExp _ _ _).
+        set (m := match _ with Pos _ => _ | _ => r end).
+        assert (H : m = r).
+        { unfold m, Z.to_int.
+          generalize (Unsigned.to_uint_nonzero pemf).
+          now case Pos.to_uint; [|intro u; case u..]. }
+        rewrite H; unfold r; clear H m r.
+        rewrite DecimalZ.of_to.
+        simpl Qnum.
+        intros Hpemf _.
+        apply f_equal; apply f_equal2; [|reflexivity].
+        rewrite !Pos2Nat.inj_iter.
+        set (n := _ pemf).
+        fold (Nat.iter n (Z.mul 10) (Z.of_int (app_int i f))).
+        fold (Nat.iter n D0 Nil).
+        rewrite <-of_int_iter_D0, to_of.
+        now rewrite norm_app_int_norm; [|induction n].
+      * simpl Qden; intros _ H; exfalso; revert H; apply Hn1.
+  - case d; clear d; intros i f; [|intro e']; simpl.
+    + case_eq (nb_digits f); [|intros nf' Hnf'];
+        [now simpl; intros _ H; exfalso; symmetry in H; revert H; apply Hn1|].
+      unfold Z.of_nat, Z.opp.
+      simpl Qden.
+      intro H; injection H; clear H; unfold Pos.pow.
+      rewrite !Pos2Nat.inj_iter.
+      intro H; generalize (Hinj _ _ H); clear H; intro H.
+      generalize (SuccNat2Pos.inj _ _ ((Pos2Nat.inj _ _ H))); clear H.
+      intro He; rewrite <-He; clear e He.
+      simpl Qnum.
+      case Nat.ltb; [left|right].
+      * now rewrite <-to_of, DecimalZ.of_to, to_of.
+      * rewrite to_of.
+        set (nif := norm _).
+        set (anif := match nif with Pos i0 => i0 | _ => _ end).
+        set (r := DecimalExp nif Nil _).
+        set (m := match _ with Pos _ => _ | _ => r end).
+        assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
+        { now unfold m; rewrite <-to_of, DecimalZ.of_to. }
+        rewrite <-to_of, !DecimalZ.of_to.
+        fold anif.
+        now rewrite SuccNat2Pos.id_succ.
+    + set (nemf := (_ - _)%Z); intro H.
+      assert (H' : exists pnemf, nemf = Z.neg pnemf); [|revert H].
+      { revert H; case nemf; [|intro pnemf..]; [..|now intros _; exists pnemf];
+          simpl Qden; intro H; exfalso; symmetry in H; revert H; apply Hn1. }
+      destruct H' as (pnemf,Hpnemf); rewrite Hpnemf.
+      simpl Qden.
+      intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter.
+      intro H; generalize (Hinj _ _ H); clear H; intro H.
+      generalize (Pos2Nat.inj _ _ H); clear H.
+      intro H; revert Hpnemf; rewrite H; clear pnemf H; intro Hnemf.
+      simpl Qnum.
+      case Nat.ltb; [left|right].
+      * now rewrite <-to_of, DecimalZ.of_to, to_of.
+      * rewrite to_of.
+        set (nif := norm _).
+        set (anif := match nif with Pos i0 => i0 | _ => _ end).
+        set (r := DecimalExp nif Nil _).
+        set (m := match _ with Pos _ => _ | _ => r end).
+        assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
+        { now unfold m; rewrite <-to_of, DecimalZ.of_to. }
+        rewrite <-to_of, !DecimalZ.of_to.
+        fold anif.
+        now rewrite SuccNat2Pos.id_succ.
+Qed.
 
 (** Some consequences *)
 
 Lemma to_decimal_inj q q' :
   to_decimal q <> None -> to_decimal q = to_decimal q' -> q = q'.
-Admitted.
+Proof.
+  intros Hnone EQ.
+  generalize (of_to q) (of_to q').
+  rewrite <-EQ.
+  revert Hnone; case to_decimal; [|now simpl].
+  now intros d _ H1 H2; rewrite <-(H1 d eq_refl), <-(H2 d eq_refl).
+Qed.
 
 Lemma to_decimal_surj d :
   exists q, to_decimal q = Some (dnorme d) \/ to_decimal q = Some (dnormf d).
-Admitted.
+Proof.
+  exists (of_decimal d). apply to_of.
+Qed.
 
 Lemma of_decimal_dnorme d : of_decimal (dnorme d) = of_decimal d.
-Admitted.
+Proof.
+  unfold of_decimal, dnorme.
+  destruct d.
+  - rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
+    case_eq (nb_digits f); [|intro nf]; intro Hnf.
+    + now simpl; rewrite app_int_nil_r, <-DecimalZ.to_of, DecimalZ.of_to.
+    + simpl; rewrite Z.sub_0_r.
+      unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
+      rewrite app_int_nil_r.
+      now rewrite <-DecimalZ.to_of, DecimalZ.of_to.
+  - rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
+    set (emf := (_ - _)%Z).
+    case_eq emf; [|intro pemf..]; intro Hemf.
+    + now simpl; rewrite app_int_nil_r, <-DecimalZ.to_of, DecimalZ.of_to.
+    + simpl.
+      set (r := DecimalExp _ Nil _).
+      set (m := match Pos.to_uint pemf with zero => _ | _ => r end).
+      assert (H : m = r); [|rewrite H; unfold r; clear m r H].
+      { generalize (Unsigned.to_uint_nonzero pemf).
+        now unfold m; case Pos.to_uint; [|intro u; case u|..]. }
+      simpl; rewrite Z.sub_0_r.
+      unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
+      rewrite app_int_nil_r.
+      now rewrite <-DecimalZ.to_of, DecimalZ.of_to.
+    + simpl.
+      unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
+      rewrite app_int_nil_r.
+      now rewrite <-DecimalZ.to_of, DecimalZ.of_to.
+Qed.
 
 Lemma of_decimal_dnormf d : of_decimal (dnormf d) = of_decimal d.
-Admitted.
+Proof.
+  rewrite <-(of_decimal_dnorme d).
+  unfold of_decimal, dnormf.
+  assert (H : match dnorme d with Decimal _ f | DecimalExp _ f _ => f end = Nil).
+  { now unfold dnorme; destruct d;
+      (case norm; intro d; [case d; [|intro u; case u|..]|]). }
+  revert H; generalize (dnorme d); clear d; intro d.
+  destruct d; intro H; rewrite H; clear H; [now simpl|].
+  case (Z.of_int e); clear e; [|intro e..].
+  - now simpl.
+  - simpl.
+    rewrite app_int_nil_r.
+    apply f_equal2; [|reflexivity].
+    rewrite app_int_nil_r.
+    rewrite <-DecimalZ.to_of, DecimalZ.of_to.
+    rewrite !Pos2Nat.inj_iter.
+    fold (Nat.iter (Pos.to_nat e) D0 Nil).
+    now rewrite of_int_iter_D0.
+  - simpl.
+    set (ai := match i with Pos _ => _ | _ => _ end).
+    rewrite app_int_nil_r.
+    case Nat.ltb_spec; intro Hei; simpl.
+    + rewrite nb_digits_del_head; [|now apply Nat.le_sub_l].
+      rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l].
+      rewrite Nat2Z.inj_sub; [|now apply le_Sn_le].
+      rewrite Z.sub_sub_distr, Z.sub_diag; simpl.
+      rewrite positive_nat_Z; simpl.
+      now revert Hei; unfold ai; case i; clear i ai; intros i Hei; simpl;
+        (rewrite app_del_tail_head; [|now apply le_Sn_le]).
+    + set (n := nb_digits _).
+      assert (H : (n = Pos.to_nat e - nb_digits ai + nb_digits ai)%nat).
+      { unfold n; induction (_ - _)%nat; [now simpl|].
+        now rewrite Unsigned.nat_iter_S; simpl; rewrite IHn0. }
+      rewrite H; clear n H.
+      rewrite Nat2Z.inj_add, (Nat2Z.inj_sub _ _ Hei).
+      rewrite <-Z.sub_sub_distr, Z.sub_diag, Z.sub_0_r.
+      rewrite positive_nat_Z; simpl.
+      rewrite <-(DecimalZ.of_to (Z.of_int (app_int _ _))), DecimalZ.to_of.
+      rewrite <-(DecimalZ.of_to (Z.of_int i)), DecimalZ.to_of.
+      apply f_equal2; [|reflexivity]; apply f_equal.
+      now unfold ai; case i; clear i ai Hei; intro i;
+        (induction (_ - _)%nat; [|rewrite <-IHn]).
+Qed.
diff --git a/theories/Numbers/DecimalZ.v b/theories/Numbers/DecimalZ.v
index 5780cf5b4f..69d8073fc7 100644
--- a/theories/Numbers/DecimalZ.v
+++ b/theories/Numbers/DecimalZ.v
@@ -73,3 +73,30 @@ Proof.
   split. apply of_inj. intros E. rewrite <- of_int_norm, E.
   apply of_int_norm.
 Qed.
+
+(** Various lemmas *)
+
+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 <-!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]. }
+  rewrite H', N.add_0_l; clear H'.
+  induction n; [now simpl; rewrite N.mul_1_r|].
+  rewrite !Unsigned.nat_iter_S, <-IHn.
+  simpl Unsigned.usize; rewrite N.pow_succ_r'.
+  rewrite !N2Z.inj_mul; simpl Z.of_N; ring.
+Qed.
+
+Lemma of_int_iter_D0 d n :
+  Z.of_int (app_int d (Nat.iter n D0 Nil)) = Nat.iter n (Z.mul 10) (Z.of_int d).
+Proof.
+  case d; clear d; intro d; simpl.
+  - now rewrite of_uint_iter_D0.
+  - rewrite of_uint_iter_D0; induction n; [now simpl|].
+    rewrite !Unsigned.nat_iter_S, <-IHn; ring.
+Qed.