[numeral notation] Remove proofs for Q

Just to get a cleaner log, this will be proved again in a few commits.

2 files changed, 19 insertions, 947 deletions

diff --git a/theories/Numbers/DecimalQ.v b/theories/Numbers/DecimalQ.v
index c51cced024..d2cd061594 100644
--- a/theories/Numbers/DecimalQ.v
+++ b/theories/Numbers/DecimalQ.v
@@ -16,62 +16,7 @@
 Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith.
 
 Lemma of_to (q:Q) : forall d, to_decimal q = Some d -> of_decimal d = q.
-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.
+Admitted.
 
 (* normalize without fractional part, for instance norme 12.3e-1 is 123e-2 *)
 Definition dnorme (d:decimal) : decimal :=
@@ -113,449 +58,38 @@ Lemma dnorme_spec d :
   | DecimalExp i Nil e => i = norm i /\ e = norm e /\ e <> Pos zero
   | _ => False
   end.
-Proof.
-  case d; clear d; intros i f; [|intro e]; unfold dnorme; simpl.
-  - set (e' := Z.to_int _).
-    case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne'].
-    + now rewrite norm_invol.
-    + set (r := DecimalExp _ _ _).
-      set (m := match norm e' with Pos zero => _ | _ => _ end).
-      replace m with r; [now unfold r; rewrite !norm_invol|].
-      unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
-      now case e''; [|intro e'''; case e'''..].
-  - set (e' := Z.to_int _).
-    case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne'].
-    + now rewrite norm_invol.
-    + set (r := DecimalExp _ _ _).
-      set (m := match norm e' with Pos zero => _ | _ => _ end).
-      replace m with r; [now unfold r; rewrite !norm_invol|].
-      unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
-      now case e''; [|intro e'''; case e'''..].
-Qed.
+Admitted.
 
 Lemma dnormf_spec d :
   match dnormf d with
   | Decimal i f => i = Neg zero \/ i = norm i
   | _ => False
   end.
-Proof.
-  case d; clear d; intros i f; [|intro e]; unfold dnormf, dnorme; simpl.
-  - set (e' := Z.to_int _).
-    case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne'].
-    + now right; rewrite norm_invol.
-    + set (r := DecimalExp _ _ _).
-      set (m := match norm e' with Pos zero => _ | _ => _ end).
-      assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
-      { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
-        now case e''; [|intro e'''; case e'''..]. }
-      rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-      case_eq (Z.of_int e'); [|intros pe'..]; intro Hpe';
-        [now right; rewrite norm_invol..|].
-      case Nat.ltb_spec.
-      * now intro H; rewrite (norm_del_tail_int_norm _ _ H); right.
-      * now intros _; case norm; intros _; [right|left].
-  - set (e' := Z.to_int _).
-    case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne'].
-    + now right; rewrite norm_invol.
-    + set (r := DecimalExp _ _ _).
-      set (m := match norm e' with Pos zero => _ | _ => _ end).
-      assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
-      { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
-        now case e''; [|intro e'''; case e'''..]. }
-      rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-      case_eq (Z.of_int e'); [|intros pe'..]; intro Hpe';
-        [now right; rewrite norm_invol..|].
-      case Nat.ltb_spec.
-      * now intro H; rewrite (norm_del_tail_int_norm _ _ H); right.
-      * now intros _; case norm; intros _; [right|left].
-Qed.
+Admitted.
 
 Lemma dnorme_invol d : dnorme (dnorme d) = dnorme d.
-Proof.
-  case d; clear d; intros i f; [|intro e]; unfold dnorme; simpl.
-  - set (e' := Z.to_int _).
-    case (int_eq_dec (norm e') (Pos zero)); intro Hne'.
-    + rewrite Hne'; simpl; rewrite app_int_nil_r, norm_invol.
-      revert Hne'.
-      rewrite <-to_of.
-      change (Pos zero) with (Z.to_int 0).
-      intro H; generalize (to_int_inj _ _ H); clear H.
-      unfold e'; rewrite DecimalZ.of_to.
-      now case f; [rewrite app_int_nil_r|..].
-    + set (r := DecimalExp _ _ _).
-      set (m := match norm e' with Pos zero => _ | _ => _ end).
-      assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
-      { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
-        now case e''; [|intro e'''; case e'''..]. }
-      rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-      unfold nb_digits, Z.of_nat; rewrite Z.sub_0_r, to_of, norm_invol.
-      rewrite app_int_nil_r, norm_invol.
-      set (r := DecimalExp _ _ _).
-      set (m := match norm e' with Pos zero => _ | _ => _ end).
-      unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
-      now case e''; [|intro e'''; case e'''..].
-  - set (e' := Z.to_int _).
-    case (int_eq_dec (norm e') (Pos zero)); intro Hne'.
-    + rewrite Hne'; simpl; rewrite app_int_nil_r, norm_invol.
-      revert Hne'.
-      rewrite <-to_of.
-      change (Pos zero) with (Z.to_int 0).
-      intro H; generalize (to_int_inj _ _ H); clear H.
-      unfold e'; rewrite DecimalZ.of_to.
-      now case f; [rewrite app_int_nil_r|..].
-    + set (r := DecimalExp _ _ _).
-      set (m := match norm e' with Pos zero => _ | _ => _ end).
-      assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
-      { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
-        now case e''; [|intro e'''; case e'''..]. }
-      rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-      unfold nb_digits, Z.of_nat; rewrite Z.sub_0_r, to_of, norm_invol.
-      rewrite app_int_nil_r, norm_invol.
-      set (r := DecimalExp _ _ _).
-      set (m := match norm e' with Pos zero => _ | _ => _ end).
-      unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl].
-      now case e''; [|intro e'''; case e'''..].
-Qed.
+Admitted.
 
 Lemma dnormf_invol d : dnormf (dnormf d) = dnormf d.
-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.
+Admitted.
 
 Lemma to_of (d:decimal) :
   to_decimal (of_decimal d) = Some (dnorme d)
   \/ to_decimal (of_decimal d) = Some (dnormf d).
-Proof.
-  unfold to_decimal.
-  pose (t10 := fun y => ((y + y~0~0)~0)%positive).
-  assert (H : exists e_den,
-             Decimal.nztail (Pos.to_uint (Qden (of_decimal d))) = (D1 Nil, e_den)).
-  { assert (H : forall p,
-               Decimal.nztail (Pos.to_uint (Pos.iter t10 1%positive p))
-               = (D1 Nil, Pos.to_nat p)).
-    { intro p; rewrite Pos2Nat.inj_iter.
-      fold (Nat.iter (Pos.to_nat p) t10 1%positive).
-      induction (Pos.to_nat p); [now simpl|].
-      rewrite DecimalPos.Unsigned.nat_iter_S.
-      unfold Pos.to_uint.
-      change (Pos.to_little_uint _)
-        with (Unsigned.to_lu (10 * N.pos (Nat.iter n t10 1%positive))).
-      rewrite Unsigned.to_ldec_tenfold.
-      revert IHn; unfold Pos.to_uint.
-      unfold Decimal.nztail; rewrite !rev_rev; simpl.
-      set (f'' := _ (Pos.to_little_uint _)).
-      now case f''; intros r n' H; inversion H. }
-    case d; intros i f; [|intro e]; unfold of_decimal; simpl.
-    - case (- Z.of_nat _)%Z; [|intro p..]; simpl; [now exists O..|].
-      exists (Pos.to_nat p); apply H.
-    - case (_ - _)%Z; [|intros p..]; simpl; [now exists O..|].
-      exists (Pos.to_nat p); apply H. }
-  generalize (DecimalPos.Unsigned.nztail_to_uint (Qden (of_decimal d))).
-  destruct H as (e, He); rewrite He; clear He; simpl.
-  assert (Hn1 : forall p, N.pos (Pos.iter t10 1%positive p) = 1%N -> False).
-  { intro p.
-    rewrite Pos2Nat.inj_iter.
-    case_eq (Pos.to_nat p); [|now simpl].
-    intro H; exfalso; apply (lt_irrefl O).
-    rewrite <-H at 2; apply Pos2Nat.is_pos. }
-  assert (Ht10inj : forall n m, t10 n = t10 m -> n = m).
-  { intros n m H; generalize (f_equal Z.pos H); clear H.
-    change (Z.pos (t10 n)) with (Z.mul 10 (Z.pos n)).
-    change (Z.pos (t10 m)) with (Z.mul 10 (Z.pos m)).
-    rewrite Z.mul_comm, (Z.mul_comm 10).
-    intro H; generalize (f_equal (fun z => Z.div z 10) H); clear H.
-    now rewrite !Z.div_mul; [|now simpl..]; intro H; inversion H. }
-  assert (Hinj : forall n m,
-             Nat.iter n t10 1%positive = Nat.iter m t10 1%positive -> n = m).
-  { induction n; [now intro m; case m|].
-    intro m; case m; [now simpl|]; clear m; intro m.
-    rewrite !Unsigned.nat_iter_S.
-    intro H; generalize (Ht10inj _ _ H); clear H; intro H.
-    now rewrite (IHn _ H). }
-  case e; clear e; [|intro e]; simpl; unfold of_decimal, dnormf, dnorme.
-  - case d; clear d; intros i f; [|intro e]; simpl.
-    + intro H; left; revert H.
-      generalize (nb_digits_pos f).
-      case f;
-        [|now clear f; intro f; intros H1 H2; exfalso; revert H1 H2;
-          case nb_digits; simpl;
-          [intros H _; apply (lt_irrefl O), H|intros n _; apply Hn1]..].
-      now intros _ _; simpl; rewrite to_of.
-    + intro H; right; revert H.
-      rewrite <-to_of, DecimalZ.of_to.
-      set (emf := (_ - _)%Z).
-      case_eq emf; [|intro pemf..].
-      * now simpl; rewrite to_of.
-      * set (r := DecimalExp _ _ _).
-        set (m := match _ with Pos _ => _ | _ => r end).
-        assert (H : m = r).
-        { unfold m, Z.to_int.
-          generalize (Unsigned.to_uint_nonzero pemf).
-          now case Pos.to_uint; [|intro u; case u..]. }
-        rewrite H; unfold r; clear H m r.
-        rewrite DecimalZ.of_to.
-        simpl Qnum.
-        intros Hpemf _.
-        apply f_equal; apply f_equal2; [|reflexivity].
-        rewrite !Pos2Nat.inj_iter.
-        set (n := _ pemf).
-        fold (Nat.iter n (Z.mul 10) (Z.of_int (app_int i f))).
-        fold (Nat.iter n D0 Nil).
-        rewrite <-of_int_iter_D0, to_of.
-        now rewrite norm_app_int_norm; [|induction n].
-      * simpl Qden; intros _ H; exfalso; revert H; apply Hn1.
-  - case d; clear d; intros i f; [|intro e']; simpl.
-    + case_eq (nb_digits f); [|intros nf' Hnf'];
-        [now simpl; intros _ H; exfalso; symmetry in H; revert H; apply Hn1|].
-      unfold Z.of_nat, Z.opp.
-      simpl Qden.
-      intro H; injection H; clear H; unfold Pos.pow.
-      rewrite !Pos2Nat.inj_iter.
-      intro H; generalize (Hinj _ _ H); clear H; intro H.
-      generalize (SuccNat2Pos.inj _ _ ((Pos2Nat.inj _ _ H))); clear H.
-      intro He; rewrite <-He; clear e He.
-      simpl Qnum.
-      case Nat.ltb; [left|right].
-      * now rewrite <-to_of, DecimalZ.of_to, to_of.
-      * rewrite to_of.
-        set (nif := norm _).
-        set (anif := match nif with Pos i0 => i0 | _ => _ end).
-        set (r := DecimalExp nif Nil _).
-        set (m := match _ with Pos _ => _ | _ => r end).
-        assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
-        { now unfold m; rewrite <-to_of, DecimalZ.of_to. }
-        rewrite <-to_of, !DecimalZ.of_to.
-        fold anif.
-        now rewrite SuccNat2Pos.id_succ.
-    + set (nemf := (_ - _)%Z); intro H.
-      assert (H' : exists pnemf, nemf = Z.neg pnemf); [|revert H].
-      { revert H; case nemf; [|intro pnemf..]; [..|now intros _; exists pnemf];
-          simpl Qden; intro H; exfalso; symmetry in H; revert H; apply Hn1. }
-      destruct H' as (pnemf,Hpnemf); rewrite Hpnemf.
-      simpl Qden.
-      intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter.
-      intro H; generalize (Hinj _ _ H); clear H; intro H.
-      generalize (Pos2Nat.inj _ _ H); clear H.
-      intro H; revert Hpnemf; rewrite H; clear pnemf H; intro Hnemf.
-      simpl Qnum.
-      case Nat.ltb; [left|right].
-      * now rewrite <-to_of, DecimalZ.of_to, to_of.
-      * rewrite to_of.
-        set (nif := norm _).
-        set (anif := match nif with Pos i0 => i0 | _ => _ end).
-        set (r := DecimalExp nif Nil _).
-        set (m := match _ with Pos _ => _ | _ => r end).
-        assert (H : m = r); [|rewrite H; unfold m, r; clear m r H].
-        { now unfold m; rewrite <-to_of, DecimalZ.of_to. }
-        rewrite <-to_of, !DecimalZ.of_to.
-        fold anif.
-        now rewrite SuccNat2Pos.id_succ.
-Qed.
+Admitted.
 
 (** Some consequences *)
 
 Lemma to_decimal_inj q q' :
   to_decimal q <> None -> to_decimal q = to_decimal q' -> q = q'.
-Proof.
-  intros Hnone EQ.
-  generalize (of_to q) (of_to q').
-  rewrite <-EQ.
-  revert Hnone; case to_decimal; [|now simpl].
-  now intros d _ H1 H2; rewrite <-(H1 d eq_refl), <-(H2 d eq_refl).
-Qed.
+Admitted.
 
 Lemma to_decimal_surj d :
   exists q, to_decimal q = Some (dnorme d) \/ to_decimal q = Some (dnormf d).
-Proof.
-  exists (of_decimal d). apply to_of.
-Qed.
+Admitted.
 
 Lemma of_decimal_dnorme d : of_decimal (dnorme d) = of_decimal d.
-Proof.
-  unfold of_decimal, dnorme.
-  destruct d.
-  - rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
-    case_eq (nb_digits f); [|intro nf]; intro Hnf.
-    + now simpl; rewrite app_int_nil_r, <-DecimalZ.to_of, DecimalZ.of_to.
-    + simpl; rewrite Z.sub_0_r.
-      unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
-      rewrite app_int_nil_r.
-      now rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-  - rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
-    set (emf := (_ - _)%Z).
-    case_eq emf; [|intro pemf..]; intro Hemf.
-    + now simpl; rewrite app_int_nil_r, <-DecimalZ.to_of, DecimalZ.of_to.
-    + simpl.
-      set (r := DecimalExp _ Nil _).
-      set (m := match Pos.to_uint pemf with zero => _ | _ => r end).
-      assert (H : m = r); [|rewrite H; unfold r; clear m r H].
-      { generalize (Unsigned.to_uint_nonzero pemf).
-        now unfold m; case Pos.to_uint; [|intro u; case u|..]. }
-      simpl; rewrite Z.sub_0_r.
-      unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
-      rewrite app_int_nil_r.
-      now rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-    + simpl.
-      unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
-      rewrite app_int_nil_r.
-      now rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-Qed.
+Admitted.
 
 Lemma of_decimal_dnormf d : of_decimal (dnormf d) = of_decimal d.
-Proof.
-  rewrite <-(of_decimal_dnorme d).
-  unfold of_decimal, dnormf.
-  assert (H : match dnorme d with Decimal _ f | DecimalExp _ f _ => f end = Nil).
-  { now unfold dnorme; destruct d;
-      (case norm; intro d; [case d; [|intro u; case u|..]|]). }
-  revert H; generalize (dnorme d); clear d; intro d.
-  destruct d; intro H; rewrite H; clear H; [now simpl|].
-  case (Z.of_int e); clear e; [|intro e..].
-  - now simpl.
-  - simpl.
-    rewrite app_int_nil_r.
-    apply f_equal2; [|reflexivity].
-    rewrite app_int_nil_r.
-    rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-    rewrite !Pos2Nat.inj_iter.
-    fold (Nat.iter (Pos.to_nat e) D0 Nil).
-    now rewrite of_int_iter_D0.
-  - simpl.
-    set (ai := match i with Pos _ => _ | _ => _ end).
-    rewrite app_int_nil_r.
-    case Nat.ltb_spec; intro Hei; simpl.
-    + rewrite nb_digits_del_head; [|now apply Nat.le_sub_l].
-      rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l].
-      rewrite Nat2Z.inj_sub; [|now apply le_Sn_le].
-      rewrite Z.sub_sub_distr, Z.sub_diag; simpl.
-      rewrite positive_nat_Z; simpl.
-      now revert Hei; unfold ai; case i; clear i ai; intros i Hei; simpl;
-        (rewrite app_del_tail_head; [|now apply le_Sn_le]).
-    + set (n := nb_digits _).
-      assert (H : (n = Pos.to_nat e - nb_digits ai + nb_digits ai)%nat).
-      { unfold n; induction (_ - _)%nat; [now simpl|].
-        now rewrite Unsigned.nat_iter_S; simpl; rewrite IHn0. }
-      rewrite H; clear n H.
-      rewrite Nat2Z.inj_add, (Nat2Z.inj_sub _ _ Hei).
-      rewrite <-Z.sub_sub_distr, Z.sub_diag, Z.sub_0_r.
-      rewrite positive_nat_Z; simpl.
-      rewrite <-(DecimalZ.of_to (Z.of_int (app_int _ _))), DecimalZ.to_of.
-      rewrite <-(DecimalZ.of_to (Z.of_int i)), DecimalZ.to_of.
-      apply f_equal2; [|reflexivity]; apply f_equal.
-      now unfold ai; case i; clear i ai Hei; intro i;
-        (induction (_ - _)%nat; [|rewrite <-IHn]).
-Qed.
+Admitted.
diff --git a/theories/Numbers/HexadecimalQ.v b/theories/Numbers/HexadecimalQ.v
index 9bf43ceb88..ce6f074d70 100644
--- a/theories/Numbers/HexadecimalQ.v
+++ b/theories/Numbers/HexadecimalQ.v
@@ -17,63 +17,7 @@ Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ.
 Require Import Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN HexadecimalZ QArith.
 
 Lemma of_to (q:Q) : forall d, to_hexadecimal q = Some d -> of_hexadecimal d = q.
-Proof.
-  cut (match to_hexadecimal q with None => True | Some d => of_hexadecimal d = q end).
-  { now case to_hexadecimal; [intros d <- d' Hd'; injection Hd'; intros ->|]. }
-  destruct q as (num, den).
-  unfold to_hexadecimal; simpl Qnum; simpl Qden.
-  generalize (HexadecimalPos.Unsigned.nztail_to_hex_uint den).
-  case Hexadecimal.nztail; intros u n.
-  change 16%N with (2^4)%N; rewrite <-N.pow_mul_r.
-  change 4%N with (N.of_nat 4); rewrite <-Nnat.Nat2N.inj_mul.
-  change 4%Z with (Z.of_nat 4); rewrite <-Nat2Z.inj_mul.
-  case u; clear u; try (intros; exact I); [| | |]; intro u;
-    (case u; clear u; [|intros; exact I..]).
-  - unfold Pos.of_hex_uint, Pos.of_hex_uint_acc; rewrite N.mul_1_l.
-    case n.
-    + unfold of_hexadecimal, app_int, app, Z.to_hex_int; simpl.
-      intro H; inversion H as (H1); clear H H1.
-      case num; [reflexivity|intro pnum; fold (rev (rev (Pos.to_hex_uint pnum)))..].
-      * rewrite rev_rev; simpl.
-        now unfold Z.of_hex_uint; rewrite HexadecimalPos.Unsigned.of_to.
-      * rewrite rev_rev; simpl.
-      now unfold Z.of_hex_uint; rewrite HexadecimalPos.Unsigned.of_to.
-    + clear n; intros n.
-      intro H; injection H; intros ->; clear H.
-      unfold of_hexadecimal.
-      rewrite DecimalZ.of_to.
-      simpl nb_digits; rewrite Nat2Z.inj_0, Z.mul_0_r, Z.sub_0_r.
-      now apply f_equal2; [rewrite app_int_nil_r, of_to|].
-  - unfold Pos.of_hex_uint, Pos.of_hex_uint_acc.
-    rewrite <-N.pow_succ_r', <-Nnat.Nat2N.inj_succ.
-    intro H; injection H; intros ->; clear H.
-    fold (4 * n)%nat.
-    change 1%Z with (Z.of_nat 1); rewrite <-Znat.Nat2Z.inj_add.
-    unfold of_hexadecimal.
-    rewrite DecimalZ.of_to.
-    simpl nb_digits; rewrite Nat2Z.inj_0, Z.mul_0_r, Z.sub_0_r.
-    now apply f_equal2; [rewrite app_int_nil_r, of_to|].
-  - change 2%Z with (Z.of_nat 2); rewrite <-Znat.Nat2Z.inj_add.
-    unfold Pos.of_hex_uint, Pos.of_hex_uint_acc.
-    change 4%N with (2^2)%N; rewrite <-N.pow_add_r.
-    change 2%N with (N.of_nat 2); rewrite <-Nnat.Nat2N.inj_add.
-    intro H; injection H; intros ->; clear H.
-    fold (4 * n)%nat.
-    unfold of_hexadecimal.
-    rewrite DecimalZ.of_to.
-    simpl nb_digits; rewrite Nat2Z.inj_0, Z.mul_0_r, Z.sub_0_r.
-    now apply f_equal2; [rewrite app_int_nil_r, of_to|].
-  - change 3%Z with (Z.of_nat 3); rewrite <-Znat.Nat2Z.inj_add.
-    unfold Pos.of_hex_uint, Pos.of_hex_uint_acc.
-    change 8%N with (2^3)%N; rewrite <-N.pow_add_r.
-    change 3%N with (N.of_nat 3); rewrite <-Nnat.Nat2N.inj_add.
-    intro H; injection H; intros ->; clear H.
-    fold (4 * n)%nat.
-    unfold of_hexadecimal.
-    rewrite DecimalZ.of_to.
-    simpl nb_digits; rewrite Nat2Z.inj_0, Z.mul_0_r, Z.sub_0_r.
-    now apply f_equal2; [rewrite app_int_nil_r, of_to|].
-Qed.
+Admitted.
 
 (* normalize without fractional part, for instance norme 0x1.2p-1 is 0x12e-5 *)
 Definition hnorme (d:hexadecimal) : hexadecimal :=
@@ -97,437 +41,31 @@ Lemma hnorme_spec d :
     i = norm i /\ e = Decimal.norm e /\ e <> Decimal.Pos Decimal.zero
   | _ => False
   end.
-Proof.
-  case d; clear d; intros i f; [|intro e]; unfold hnorme; simpl.
-  - case_eq (nb_digits f); [now simpl; rewrite norm_invol|]; intros nf Hnf.
-    split; [now simpl; rewrite norm_invol|].
-    unfold Z.of_nat.
-    now rewrite <-!DecimalZ.to_of, !DecimalZ.of_to.
-  - set (e' := (_ - _)%Z).
-    case_eq e'; [|intro pe'..]; intro He'.
-    + now rewrite norm_invol.
-    + rewrite Pos2Nat.inj_iter.
-      set (ne' := Pos.to_nat pe').
-      fold (Nat.iter ne' double (norm (app_int i f))).
-      induction ne'; [now simpl; rewrite norm_invol|].
-      now rewrite Unsigned.nat_iter_S, <-double_norm, IHne', norm_invol.
-    + split; [now rewrite norm_invol|].
-      split; [now rewrite DecimalFacts.norm_invol|].
-      rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-      change (Decimal.Pos _) with (Z.to_int 0).
-      now intro H; generalize (DecimalZ.to_int_inj _ _ H).
-Qed.
+Admitted.
 
 Lemma hnorme_invol d : hnorme (hnorme d) = hnorme d.
-Proof.
-  case d; clear d; intros i f; [|intro e]; unfold hnorme; simpl.
-  - case_eq (nb_digits f); [now simpl; rewrite app_int_nil_r, norm_invol|].
-    intros nf Hnf.
-    unfold Z.of_nat.
-    simpl.
-    set (pnf := Pos.to_uint _).
-    set (nz := Decimal.nzhead pnf).
-    assert (Hnz : nz <> Decimal.Nil).
-    { unfold nz, pnf.
-      rewrite <-DecimalFacts.unorm_0.
-      rewrite <-DecimalPos.Unsigned.to_of.
-      rewrite DecimalPos.Unsigned.of_to.
-      change Decimal.zero with (N.to_uint 0).
-      now intro H; generalize (DecimalN.Unsigned.to_uint_inj _ _ H). }
-    set (m := match nz with Decimal.Nil => _ | _ => _ end).
-    assert (Hm : m = (Decimal.Neg (Decimal.unorm pnf))).
-    { now revert Hnz; unfold m, nz, Decimal.unorm; fold nz; case nz. }
-    rewrite Hm; unfold pnf.
-    rewrite <-DecimalPos.Unsigned.to_of, DecimalPos.Unsigned.of_to.
-    simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to.
-    rewrite Z.sub_0_r; simpl.
-    fold pnf; fold nz; fold m; rewrite Hm; unfold pnf.
-    rewrite <-DecimalPos.Unsigned.to_of, DecimalPos.Unsigned.of_to.
-    now rewrite app_int_nil_r, norm_invol.
-  - set (e' := (_ - _)%Z).
-    case_eq e'; [|intro pe'..]; intro Hpe'.
-    + now simpl; rewrite app_int_nil_r, norm_invol.
-    + simpl; rewrite app_int_nil_r.
-      apply f_equal2; [|reflexivity].
-      rewrite Pos2Nat.inj_iter.
-      set (ne' := Pos.to_nat pe').
-      fold (Nat.iter ne' double (norm (app_int i f))).
-      induction ne'; [now simpl; rewrite norm_invol|].
-      now rewrite Unsigned.nat_iter_S, <-double_norm, IHne'.
-    + rewrite <-DecimalZ.to_of, !DecimalZ.of_to; simpl.
-      rewrite app_int_nil_r, norm_invol.
-      set (pnf := Pos.to_uint _).
-      set (nz := Decimal.nzhead pnf).
-      assert (Hnz : nz <> Decimal.Nil).
-      { unfold nz, pnf.
-        rewrite <-DecimalFacts.unorm_0.
-        rewrite <-DecimalPos.Unsigned.to_of.
-        rewrite DecimalPos.Unsigned.of_to.
-        change Decimal.zero with (N.to_uint 0).
-        now intro H; generalize (DecimalN.Unsigned.to_uint_inj _ _ H). }
-      set (m := match nz with Decimal.Nil => _ | _ => _ end).
-      assert (Hm : m = (Decimal.Neg (Decimal.unorm pnf))).
-      { now revert Hnz; unfold m, nz, Decimal.unorm; fold nz; case nz. }
-      rewrite Hm; unfold pnf.
-      now rewrite <-DecimalPos.Unsigned.to_of, DecimalPos.Unsigned.of_to.
-Qed.
+Admitted.
 
 Lemma to_of (d:hexadecimal) :
   to_hexadecimal (of_hexadecimal d) = Some (hnorme d).
-Proof.
-  unfold to_hexadecimal.
-  pose (t10 := fun y => (y~0~0~0~0)%positive).
-  assert (H : exists h e_den,
-             Hexadecimal.nztail (Pos.to_hex_uint (Qden (of_hexadecimal d)))
-             = (h, e_den)
-             /\ (h = D1 Nil \/ h = D2 Nil \/ h = D4 Nil \/ h = D8 Nil)).
-  { assert (H : forall p,
-               Hexadecimal.nztail (Pos.to_hex_uint (Pos.iter (Pos.mul 2) 1%positive p))
-               = ((match (Pos.to_nat p) mod 4 with 0%nat => D1 | 1 => D2 | 2 => D4 | _ => D8 end)%nat Nil,
-                  (Pos.to_nat p / 4)%nat)).
-    { intro p; clear d; rewrite Pos2Nat.inj_iter.
-      fold (Nat.iter (Pos.to_nat p) (Pos.mul 2) 1%positive).
-      set (n := Pos.to_nat p).
-      fold (Nat.iter n t10 1%positive).
-      set (nm4 := (n mod 4)%nat); set (nd4 := (n / 4)%nat).
-      rewrite (Nat.div_mod n 4); [|now simpl].
-      unfold nm4, nd4; clear nm4 nd4.
-      generalize (Nat.mod_upper_bound n 4 ltac:(now simpl)).
-      generalize (n mod 4); generalize (n / 4)%nat.
-      intros d r Hr; clear p n.
-      induction d.
-      { simpl; revert Hr.
-        do 4 (case r; [now simpl|clear r; intro r]).
-        intro H; exfalso.
-        now do 4 (generalize (lt_S_n _ _ H); clear H; intro H). }
-      rewrite Nat.mul_succ_r, <-Nat.add_assoc, (Nat.add_comm 4), Nat.add_assoc.
-      rewrite (Nat.add_comm _ 4).
-      change (4 + _)%nat with (S (S (S (S (4 * d + r))))).
-      rewrite !Unsigned.nat_iter_S.
-      rewrite !Pos.mul_assoc.
-      unfold Pos.to_hex_uint.
-      change (2 * 2 *  2 * 2)%positive with 0x10%positive.
-      set (n := Nat.iter _ _ _).
-      change (Pos.to_little_hex_uint _) with (Unsigned.to_lu (16 * N.pos n)).
-      rewrite Unsigned.to_lhex_tenfold.
-      unfold Hexadecimal.nztail; rewrite rev_rev.
-      rewrite <-(rev_rev (Unsigned.to_lu _)).
-      set (m := _ (rev _)).
-      replace m with (let (r, n) := let (r, n) := m in (rev r, n) in (rev r, n)).
-      2:{ now case m; intros r' n'; rewrite rev_rev. }
-      change (let (r, n) := m in (rev r, n))
-        with (Hexadecimal.nztail (Pos.to_hex_uint n)).
-      now unfold n; rewrite IHd, rev_rev; clear n m. }
-    unfold of_hexadecimal.
-    case d; intros i f; [|intro e]; unfold of_hexadecimal; simpl.
-    - case (Z.of_nat _)%Z; [|intro p..];
-        [now exists (D1 Nil), O; split; [|left]
-        | |now exists (D1 Nil), O; split; [|left]].
-      exists (D1 Nil), (Pos.to_nat p).
-      split; [|now left]; simpl.
-      change (Pos.iter _ _ _) with (Pos.iter (Pos.mul 2) 1%positive (4 * p)).
-      rewrite H.
-      rewrite Pos2Nat.inj_mul, Nat.mul_comm, Nat.div_mul; [|now simpl].
-      now rewrite Nat.mod_mul; [|now simpl].
-    - case (_ - _)%Z; [|intros p..]; [now exists (D1 Nil), O; split; [|left]..|].
-      simpl Qden; rewrite H.
-      eexists; eexists; split; [reflexivity|].
-      case (_ mod _); [now left|intro n].
-      case n; [now right; left|clear n; intro n].
-      case n; [now right; right; left|clear n; intro n].
-      now right; right; right. }
-  generalize (HexadecimalPos.Unsigned.nztail_to_hex_uint (Qden (of_hexadecimal d))).
-  destruct H as (h, (e, (He, Hh))); rewrite He; clear He.
-  assert (Hn1 : forall p, N.pos (Pos.iter (Pos.mul 2) 1%positive p) = 1%N -> False).
-  { intro p.
-    rewrite Pos2Nat.inj_iter.
-    case_eq (Pos.to_nat p); [|now simpl].
-    intro H; exfalso; apply (lt_irrefl O).
-    rewrite <-H at 2; apply Pos2Nat.is_pos. }
-  assert (H16_2 : forall p, (16^p = 2^(4 * p))%positive).
-  { intro p.
-    apply (@f_equal _ _ (fun z => match z with Z.pos p => p | _ => 1%positive end)
-                    (Z.pos _) (Z.pos _)).
-    rewrite !Pos2Z.inj_pow_pos, !Z.pow_pos_fold, Pos2Z.inj_mul.
-    now change 16%Z with (2^4)%Z; rewrite <-Z.pow_mul_r. }
-  assert (HN16_2 : forall n, (16^n = 2^(4 * n))%N).
-  { intro n.
-    apply N2Z.inj; rewrite !N2Z.inj_pow, N2Z.inj_mul.
-    change (Z.of_N 16) with (2^4)%Z.
-    now rewrite <-Z.pow_mul_r; [| |apply N2Z.is_nonneg]. }
-  assert (Hn1' : forall p, N.pos (Pos.iter (Pos.mul 16) 1%positive p) = 1%N -> False).
-  { intro p; fold (16^p)%positive; rewrite H16_2; apply Hn1. }
-  assert (Ht10inj : forall n m, t10 n = t10 m -> n = m).
-  { intros n m H; generalize (f_equal Z.pos H); clear H.
-    change (Z.pos (t10 n)) with (Z.mul 0x10 (Z.pos n)).
-    change (Z.pos (t10 m)) with (Z.mul 0x10 (Z.pos m)).
-    rewrite Z.mul_comm, (Z.mul_comm 0x10).
-    intro H; generalize (f_equal (fun z => Z.div z 0x10) H); clear H.
-    now rewrite !Z.div_mul; [|now simpl..]; intro H; inversion H. }
-  assert (Ht2inj : forall n m, Pos.mul 2 n = Pos.mul 2 m -> n = m).
-  { intros n m H; generalize (f_equal Z.pos H); clear H.
-    change (Z.pos (Pos.mul 2 n)) with (Z.mul 2 (Z.pos n)).
-    change (Z.pos (Pos.mul 2 m)) with (Z.mul 2 (Z.pos m)).
-    rewrite Z.mul_comm, (Z.mul_comm 2).
-    intro H; generalize (f_equal (fun z => Z.div z 2) H); clear H.
-    now rewrite !Z.div_mul; [|now simpl..]; intro H; inversion H. }
-  assert (Hinj : forall n m,
-             Nat.iter n (Pos.mul 2) 1%positive = Nat.iter m (Pos.mul 2) 1%positive
-             -> n = m).
-  { induction n; [now intro m; case m|].
-    intro m; case m; [now simpl|]; clear m; intro m.
-    rewrite !Unsigned.nat_iter_S.
-    intro H; generalize (Ht2inj _ _ H); clear H; intro H.
-    now rewrite (IHn _ H). }
-  change 4%Z with (Z.of_nat 4); rewrite <-Nat2Z.inj_mul.
-  change 1%Z with (Z.of_nat 1); rewrite <-Nat2Z.inj_add.
-  change 2%Z with (Z.of_nat 2); rewrite <-Nat2Z.inj_add.
-  change 3%Z with (Z.of_nat 3); rewrite <-Nat2Z.inj_add.
-  destruct Hh as [Hh|[Hh|[Hh|Hh]]]; rewrite Hh; clear h Hh.
-  - case e; clear e; [|intro e]; simpl; unfold of_hexadecimal, hnorme.
-    + case d; clear d; intros i f; [|intro e].
-      * generalize (nb_digits_pos f).
-        case f;
-          [|now clear f; intro f; intros H1 H2; exfalso; revert H1 H2;
-            case nb_digits;
-            [intros H _; apply (lt_irrefl O), H|intros n _; apply Hn1]..].
-        now intros _ _; simpl; rewrite to_of.
-      * rewrite <-DecimalZ.to_of, DecimalZ.of_to.
-        set (emf := (_ - _)%Z).
-        case_eq emf; [|intro pemf..].
-        ++ now simpl; rewrite to_of.
-        ++ intros Hemf _; simpl.
-           apply f_equal, f_equal2; [|reflexivity].
-           rewrite !Pos2Nat.inj_iter.
-           fold (Nat.iter (Pos.to_nat pemf) (Z.mul 2) (Z.of_hex_int (app_int i f))).
-           fold (Nat.iter (Pos.to_nat pemf) double (norm (app_int i f))).
-           induction Pos.to_nat; [now simpl; rewrite HexadecimalZ.to_of|].
-           now rewrite !Unsigned.nat_iter_S, <-IHn, double_to_hex_int.
-        ++ simpl Qden; intros _ H; exfalso; revert H; apply Hn1.
-    + case d; clear d; intros i f; [|intro e'].
-      * simpl; case_eq (nb_digits f); [|intros nf' Hnf'];
-          [now simpl; intros _ H; exfalso; symmetry in H; revert H; apply Hn1'|].
-        unfold Z.of_nat, Z.opp, Qnum, Qden.
-        rewrite H16_2.
-        fold (Pos.mul 2); fold (2^(Pos.of_succ_nat nf')~0~0)%positive.
-        intro H; injection H; clear H.
-        unfold Pos.pow; rewrite !Pos2Nat.inj_iter.
-        intro H; generalize (Hinj _ _ H); clear H; intro H.
-        generalize (Pos2Nat.inj _ _ H); clear H; intro H; injection H.
-        clear H; intro H; generalize (SuccNat2Pos.inj _ _ H); clear H.
-        intros <-.
-        rewrite to_of.
-        rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
-        do 4 apply f_equal.
-        apply Pos2Nat.inj.
-        rewrite SuccNat2Pos.id_succ.
-        change (_~0)%positive with (4 * Pos.of_succ_nat nf')%positive.
-        now rewrite Pos2Nat.inj_mul, SuccNat2Pos.id_succ.
-      * set (nemf := (_ - _)%Z); intro H.
-        assert (H' : exists pnemf, nemf = Z.neg pnemf); [|revert H].
-        { revert H; case nemf; [|intro pnemf..]; [..|now intros _; exists pnemf];
-            simpl Qden; intro H; exfalso; symmetry in H; revert H; apply Hn1'. }
-        destruct H' as (pnemf,Hpnemf); rewrite Hpnemf.
-        unfold Qnum, Qden.
-        rewrite H16_2.
-        intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter.
-        intro H; generalize (Hinj _ _ H); clear H; intro H.
-        generalize (Pos2Nat.inj _ _ H); clear H.
-        intro H; revert Hpnemf; rewrite H; clear pnemf H; intro Hnemf.
-        rewrite to_of.
-        rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
-        do 4 apply f_equal.
-        apply Pos2Nat.inj.
-        rewrite SuccNat2Pos.id_succ.
-        change (_~0)%positive with (4 * Pos.of_succ_nat e)%positive.
-        now rewrite Pos2Nat.inj_mul, SuccNat2Pos.id_succ.
-  - simpl Pos.of_hex_uint.
-    rewrite HN16_2.
-    rewrite <-N.pow_succ_r; [|now apply N.le_0_l].
-    rewrite <-N.succ_pos_spec.
-    case d; clear d; intros i f; [|intro e']; unfold of_hexadecimal, hnorme.
-    + set (em4f := (_ - _)%Z).
-      case_eq em4f; [|intros pem4f..]; intro Hpem4f;
-        [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|].
-      unfold Qnum, Qden.
-      intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter.
-      intro H; generalize (Hinj _ _ H); clear H; intro H.
-      generalize (Pos2Nat.inj _ _ H); clear H; intros ->.
-      rewrite to_of.
-      rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
-      do 4 apply f_equal.
-      apply Pos2Nat.inj.
-      rewrite SuccNat2Pos.id_succ.
-      case e; [now simpl|intro e'']; simpl.
-      unfold Pos.to_nat; simpl.
-      now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm.
-    + set (em4f := (_ - _)%Z).
-      case_eq em4f; [|intros pem4f..]; intro Hpem4f;
-        [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|].
-      unfold Qnum, Qden.
-      intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter.
-      intro H; generalize (Hinj _ _ H); clear H; intro H.
-      generalize (Pos2Nat.inj _ _ H); clear H; intros ->.
-      rewrite to_of.
-      rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
-      do 4 apply f_equal.
-      apply Pos2Nat.inj.
-      rewrite SuccNat2Pos.id_succ.
-      case e; [now simpl|intro e'']; simpl.
-      unfold Pos.to_nat; simpl.
-      now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm.
-  - simpl Pos.of_hex_uint.
-    rewrite HN16_2.
-    change 4%N with (2 * 2)%N at 1; rewrite <-!N.mul_assoc.
-    do 2 (rewrite <-N.pow_succ_r; [|now apply N.le_0_l]).
-    rewrite <-N.succ_pos_spec.
-    case d; clear d; intros i f; [|intro e']; unfold of_hexadecimal, hnorme.
-    + set (em4f := (_ - _)%Z).
-      case_eq em4f; [|intros pem4f..]; intro Hpem4f;
-        [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|].
-      unfold Qnum, Qden.
-      intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter.
-      intro H; generalize (Hinj _ _ H); clear H; intro H.
-      generalize (Pos2Nat.inj _ _ H); clear H; intros ->.
-      rewrite to_of.
-      rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
-      do 4 apply f_equal.
-      apply Pos2Nat.inj.
-      rewrite <-SuccNat2Pos.inj_succ.
-      rewrite SuccNat2Pos.id_succ.
-      case e; [now simpl|intro e'']; simpl.
-      unfold Pos.to_nat; simpl.
-      now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm.
-    + set (em4f := (_ - _)%Z).
-      case_eq em4f; [|intros pem4f..]; intro Hpem4f;
-        [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|].
-      unfold Qnum, Qden.
-      intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter.
-      intro H; generalize (Hinj _ _ H); clear H; intro H.
-      generalize (Pos2Nat.inj _ _ H); clear H; intros ->.
-      rewrite to_of.
-      rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
-      do 4 apply f_equal.
-      apply Pos2Nat.inj.
-      rewrite <-SuccNat2Pos.inj_succ.
-      rewrite SuccNat2Pos.id_succ.
-      case e; [now simpl|intro e'']; simpl.
-      unfold Pos.to_nat; simpl.
-      now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm.
-  - simpl Pos.of_hex_uint.
-    rewrite HN16_2.
-    change 8%N with (2 * 2 * 2)%N; rewrite <-!N.mul_assoc.
-    do 3 (rewrite <-N.pow_succ_r; [|now apply N.le_0_l]).
-    rewrite <-N.succ_pos_spec.
-    case d; clear d; intros i f; [|intro e']; unfold of_hexadecimal, hnorme.
-    + set (em4f := (_ - _)%Z).
-      case_eq em4f; [|intros pem4f..]; intro Hpem4f;
-        [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|].
-      unfold Qnum, Qden.
-      intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter.
-      intro H; generalize (Hinj _ _ H); clear H; intro H.
-      generalize (Pos2Nat.inj _ _ H); clear H; intros ->.
-      rewrite to_of.
-      rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
-      do 4 apply f_equal.
-      apply Pos2Nat.inj.
-      rewrite <-!SuccNat2Pos.inj_succ.
-      rewrite SuccNat2Pos.id_succ.
-      case e; [now simpl|intro e'']; simpl.
-      unfold Pos.to_nat; simpl.
-      now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm.
-    + set (em4f := (_ - _)%Z).
-      case_eq em4f; [|intros pem4f..]; intro Hpem4f;
-        [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|].
-      unfold Qnum, Qden.
-      intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter.
-      intro H; generalize (Hinj _ _ H); clear H; intro H.
-      generalize (Pos2Nat.inj _ _ H); clear H; intros ->.
-      rewrite to_of.
-      rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl.
-      do 4 apply f_equal.
-      apply Pos2Nat.inj.
-      rewrite <-!SuccNat2Pos.inj_succ.
-      rewrite SuccNat2Pos.id_succ.
-      case e; [now simpl|intro e'']; simpl.
-      unfold Pos.to_nat; simpl.
-      now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm.
-Qed.
+Admitted.
 
 (** Some consequences *)
 
 Lemma to_hexadecimal_inj q q' :
   to_hexadecimal q <> None -> to_hexadecimal q = to_hexadecimal q' -> q = q'.
-Proof.
-  intros Hnone EQ.
-  generalize (of_to q) (of_to q').
-  rewrite <-EQ.
-  revert Hnone; case to_hexadecimal; [|now simpl].
-  now intros d _ H1 H2; rewrite <-(H1 d eq_refl), <-(H2 d eq_refl).
-Qed.
+Admitted.
 
 Lemma to_hexadecimal_surj d : exists q, to_hexadecimal q = Some (hnorme d).
-Proof.
-  exists (of_hexadecimal d). apply to_of.
-Qed.
+Admitted.
 
 Lemma of_hexadecimal_hnorme d : of_hexadecimal (hnorme d) = of_hexadecimal d.
-Proof.
-  unfold of_hexadecimal, hnorme.
-  destruct d.
-  - simpl Z.of_int; unfold Z.of_uint, Z.of_N, Pos.of_uint.
-    rewrite Z.sub_0_l.
-    set (n4f := (- _)%Z).
-    case_eq n4f; [|intro pn4f..]; intro Hn4f.
-    + apply f_equal2; [|reflexivity].
-      rewrite app_int_nil_r.
-      now rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to.
-    + apply f_equal2; [|reflexivity].
-      rewrite app_int_nil_r.
-      generalize (app_int i f); intro i'.
-      rewrite !Pos2Nat.inj_iter.
-      generalize (Pos.to_nat pn4f); intro n.
-      fold (Nat.iter n double (norm i')).
-      fold (Nat.iter n (Z.mul 2) (Z.of_hex_int i')).
-      induction n; [now simpl; rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to|].
-      now rewrite !Unsigned.nat_iter_S, <-IHn, of_hex_int_double.
-    + unfold nb_digits, Z.of_nat.
-      rewrite Z.mul_0_r, Z.sub_0_r.
-      rewrite <-DecimalZ.to_of, !DecimalZ.of_to.
-      rewrite app_int_nil_r.
-      now rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to.
-  - set (nem4f := (_ - _)%Z).
-    case_eq nem4f; [|intro pnem4f..]; intro Hnem4f.
-    + apply f_equal2; [|reflexivity].
-      rewrite app_int_nil_r.
-      now rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to.
-    + apply f_equal2; [|reflexivity].
-      rewrite app_int_nil_r.
-      generalize (app_int i f); intro i'.
-      rewrite !Pos2Nat.inj_iter.
-      generalize (Pos.to_nat pnem4f); intro n.
-      fold (Nat.iter n double (norm i')).
-      fold (Nat.iter n (Z.mul 2) (Z.of_hex_int i')).
-      induction n; [now simpl; rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to|].
-      now rewrite !Unsigned.nat_iter_S, <-IHn, of_hex_int_double.
-    + unfold nb_digits, Z.of_nat.
-      rewrite Z.mul_0_r, Z.sub_0_r.
-      rewrite <-DecimalZ.to_of, !DecimalZ.of_to.
-      rewrite app_int_nil_r.
-      now rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to.
-Qed.
+Admitted.
 
 Lemma of_inj d d' :
   of_hexadecimal d = of_hexadecimal d' -> hnorme d = hnorme d'.
-Proof.
-  intros.
-  cut (Some (hnorme d) = Some (hnorme d')); [now intro H'; injection H'|].
-  rewrite <- !to_of. now f_equal.
-Qed.
+Admitted.
 
 Lemma of_iff d d' :
   of_hexadecimal d = of_hexadecimal d' <-> hnorme d = hnorme d'.
-Proof.
-  split. apply of_inj. intros E. rewrite <- of_hexadecimal_hnorme, E.
-  apply of_hexadecimal_hnorme.
-Qed.
+Admitted.