diff --git a/banach.v b/banach.v
index 5e549e0..6af2356 100644
--- a/banach.v
+++ b/banach.v
@@ -753,7 +753,31 @@ Module banach.
       apply converge_func_correct.
     Qed.
 
-    
+    Lemma dist_converge_func_step_r : forall (f : T->R), dist f (step_f converge_func) = dist f converge_func.
+    Proof.
+      intros.
+      unfold max_dist.
+      apply mapmax_ne_ext. intros.
+      rewrite rec_fixpoint. auto.
+    Qed.
+
+    Lemma dist_fixpoint_step_ub: forall (f : T->R),
+        ((1+ - q) * dist f converge_func <= dist f (step_f f)).
+    Proof.
+      intros.
+      rewrite plus_mult_distr_r.
+      enough(dist f converge_func  <=  dist f (step_f f) + q * dist f converge_func).
+      { 
+        replace(_ <= _) with (1 * dist f converge_func + - q * dist f converge_func <= dist f (step_f f))%R; auto.
+        replace(_ <= _) with (dist f converge_func <= dist f (step_f f) + q * dist f converge_func)%R in H; auto.
+        lra.
+      }
+      apply le_trans with (dist f (step_f f) + dist (step_f f) converge_func).
+        apply dist_triangle. apply Numeric_Props_R. 
+      apply plus_le_compat_l.
+      rewrite <- dist_converge_func_step_r.
+      apply is_contr.
+    Qed.
 
   End banach_R.
 
@@ -780,9 +804,9 @@ Module banach.
       apply H1. auto.
   Qed.    
     
+  
 
-
-  Record R_Nt_relation {Nt : Type} `{Numerics.Numeric Nt} : Type :=
+  Record R_Nt_relation {Nt : Type} `{numeric_t : Numerics.Numeric Nt} `{@Numerics.Numeric_R_inj Nt numeric_t} : Type :=
     R_Nt_relation_mk {
       relation_contr : @contraction_func R _;  
       Nt_step : ((x_t relation_contr) -> Nt) -> ((x_t relation_contr) -> Nt);
@@ -791,7 +815,7 @@ Module banach.
     }.
 
   Section banach_Nt_R.
-    Context {Nt:Type} `{Numerics.Numeric Nt}.
+    Context {Nt:Type} `{Numerics.Numeric Nt} `{Nt_R_inj : @Numerics.Numeric_R_inj Nt H}.
     Variable relation : R_Nt_relation.
 
 
diff --git a/dyadic.v b/dyadic.v
index 70577b7..f75ddc3 100644
--- a/dyadic.v
+++ b/dyadic.v
@@ -429,33 +429,80 @@ Qed.
 Definition DOle (d1 d2 : DO) : Prop :=
   Qle (DO_to_Q d1) (DO_to_Q d2).  
 
-(*TODO: There's probably a more efficient way to implement the following:*)
 Definition DOle_bool (d1 d2 : DO) : bool :=
-  Qle_bool (DO_to_Q d1) (DO_to_Q d2).
+  Z.leb (num (DOsub d1 d2)) 0 .
+
+Lemma DO_num_neg_iff: forall d, (DO_to_Q d < 0)%Q <-> (num d < 0)%Z.
+Proof.
+    intros.
+    split; intros;
+      unfold Qlt in *; simpl in *; lia.
+Qed.
+
+Lemma DO_num_leq_0_iff: forall d, (DO_to_Q d <= 0)%Q <-> (num d <= 0)%Z.
+Proof.
+    intros.
+    split; intros;
+      unfold Qle in *; simpl in *; lia.
+Qed.
+
 
 Lemma DOle_bool_iff d1 d2 : (DOle_bool d1 d2 = true) <-> DOle d1 d2.
 Proof.
   unfold DOle_bool, DOle.
-  apply Qle_bool_iff.
+  split; intros.
+  {
+    setoid_replace (DO_to_Q d2) with (DO_to_Q d2 + 0)%Q using relation Qeq.
+    2: unfold Qeq; simpl; lia.
+    setoid_replace (DO_to_Q d1) with (DO_to_Q d2 + (DO_to_Q d1 - DO_to_Q d2))%Q using relation Qeq.
+    2: unfold Qeq; simpl; lia.
+    rewrite Qplus_le_r.
+    rewrite <- DOsub_ok.
+    apply DO_num_leq_0_iff.
+    apply Z.leb_le.
+    auto.
+  }
+  setoid_replace (DO_to_Q d2) with (DO_to_Q d2 + 0)%Q using relation Qeq in H.
+  2: unfold Qeq; simpl; lia.
+  setoid_replace (DO_to_Q d1) with (DO_to_Q d2 + (DO_to_Q d1 - DO_to_Q d2))%Q using relation Qeq in H.
+  2: unfold Qeq; simpl; lia.
+  rewrite Qplus_le_r in H.
+  rewrite <- DOsub_ok in H.
+  apply DO_num_leq_0_iff in H.
+  apply Z.leb_le in H.
+  auto.
 Qed.
 
 Definition DOlt (d1 d2 : DO) : Prop :=
   Qlt (DO_to_Q d1) (DO_to_Q d2).  
 
 Definition DOlt_bool (d1 d2 : DO) : bool :=
-  match DO_to_Q d1 ?= DO_to_Q d2 with
-  | Lt => true
-  | _ => false
-  end.
+  Z.ltb (num (DOsub d1 d2)) 0 .
 
 Lemma DOlt_bool_iff d1 d2 : (DOlt_bool d1 d2 = true) <-> DOlt d1 d2.
 Proof.
-  unfold DOlt_bool; split.
-  destruct (Qcompare_spec (DO_to_Q d1) (DO_to_Q d2));
-    try solve[inversion 1|auto].
-  unfold DOlt; rewrite Qlt_alt; intros ->; auto.
+  unfold DOlt_bool; unfold DOlt; split; intros.
+  {
+    setoid_replace (DO_to_Q d2) with (DO_to_Q d2 + 0)%Q using relation Qeq.
+    2: unfold Qeq; simpl; lia.
+    setoid_replace (DO_to_Q d1) with (DO_to_Q d2 + (DO_to_Q d1 - DO_to_Q d2))%Q using relation Qeq.
+    2: unfold Qeq; simpl; lia.
+    rewrite Qplus_lt_r.
+    rewrite <- DOsub_ok.
+    apply DO_num_neg_iff.
+    apply Z.ltb_lt. auto.
+  }
+  setoid_replace (DO_to_Q d2) with (DO_to_Q d2 + 0)%Q using relation Qeq in H.
+  2: unfold Qeq; simpl; lia.
+  setoid_replace (DO_to_Q d1) with (DO_to_Q d2 + (DO_to_Q d1 - DO_to_Q d2))%Q using relation Qeq in H.
+  2: unfold Qeq; simpl; lia.
+  rewrite Qplus_lt_r in H.
+  rewrite <- DOsub_ok in H.
+  apply DO_num_neg_iff in H.
+  apply Z.ltb_lt. auto.
 Qed.  
 
+
 Lemma DOeq_dec (d1 d2 : DO) : {d1=d2} + {d1<>d2}.
 Proof.
   destruct d1, d2.
@@ -1198,6 +1245,7 @@ Proof.
     apply Zodd_not_Zeven in H; contradiction. }
   destruct (DOred' x y); simpl in H|-*; rewrite H; auto.
 Qed.  
+
     
 Lemma DOred_idem d : DOred (DOred d) = DOred d.
 Proof.
@@ -1232,6 +1280,26 @@ Proof.
 Qed.  
 
 
+Lemma DOred_complete_converse d1 d2 :
+  DOred d1 = DOred d2 ->
+  DO_to_Q d1 == DO_to_Q d2.
+Proof.
+  intros.
+  rewrite <- DOred_correct.
+  rewrite <- (@DOred_correct d2).
+  rewrite H.
+  apply Qeq_refl.
+Qed.
+
+Lemma DO_lt_le_dec: forall d1 d2, {d1 < d2} + {d2 <= d1}.
+Proof.
+  intros.  
+  unfold DOlt.
+  unfold DOle.
+  apply Qlt_le_dec.
+Qed.
+
+
 Module DORed.
   Record t : Type :=
     mk { d :> DO;
@@ -1242,7 +1310,7 @@ Module DORed.
   Program Definition t0 := mk 0 _.
 
   Program Definition t1 := mk 1 _.
-  
+
   Program Definition add (d1 d2 : t) : t :=
     mk (DOred (DOadd d1.(d) d2.(d))) _.
   Next Obligation.
@@ -1289,7 +1357,18 @@ Module DORed.
     intros H; assert (H2: x1 = x2).
     { rewrite <-pf1, <-pf2; apply DOred_complete; auto. }
     generalize pf1 pf2; rewrite H2; intros; f_equal; apply proof_irrelevance.
-  Qed.    
+  Qed.
+
+  Lemma DOred_eq_weak: forall (d1 d2 : t), (d d1 = d d2) -> d1 = d2.
+  Proof.
+    intros.
+    apply DOred_eq.
+    destruct d1. destruct d2.
+    simpl.
+    simpl in H.
+    rewrite H.
+    apply Qeq_refl.
+  Qed.
   
   Lemma addP d1 d2 :
     DO_to_Q (d (add d1 d2)) == (DO_to_Q (d d1) + DO_to_Q (d d2))%Q.
@@ -1639,42 +1718,59 @@ Module DORed.
   Lemma natPowRec: forall (d : t) (n : nat), natPow d (S n) = mult d (natPow d n).
   Proof. auto. Qed.
 
-  Lemma lt_le_dec: forall d1 d2, {d1 < d2} + {d2 <= d1}.
-  Proof. intros. unfold DOle. unfold DOlt. apply Qlt_le_dec. Qed.
 
+  (* Lemma lt_Qeq: forall d1 d2 d3 d4 : DO, DO_to_Q d1 == DO_to_Q d3 -> DO_to_Q d2 == DO_to_Q d4 -> (d1 < d2 <-> d3 < d4).
+  Proof.
+    intros.
+    split; intros.
+      unfold DOlt. rewrite <-  H. lia.
+      rewrite H.
+ *)
+  
+
+  Lemma num_ge0_iff: forall d, (0 <= DO_to_Q d)%Q <-> (0 <= num d)%Z.
+  Proof.
+    intros.
+    split; intros;
+      unfold Qle in *; simpl in *; lia.
+  Qed.
 
   Lemma le_lt_dec: forall d1 d2,  {d1 <= d2} + {d2 < d1}.
   Proof.
     intros.
-    unfold DOle.
-    unfold DOlt.
-    destruct Qlt_le_dec with (DO_to_Q d2) (DO_to_Q d1); auto.
+    destruct (DO_lt_le_dec d2 d1); auto.
   Qed.
 
+  Lemma num_0_iff: forall d, num d = 0%Z <-> DO_to_Q d == 0.
+  Proof.
+    intros.
+    split; intros;
+      unfold Qeq in *; simpl in *; lia.
+  Qed.
 
   Lemma eq_dec: forall d1 d2 : t, {d1 = d2} + {d1 <> d2}.
   Proof.
     intros.
-    destruct DOeq_dec with (d d1) (d d2).
-    { 
-      left. 
-      destruct d1,d2.
-      simpl in e.
-      generalize pf0 pf1.
-      rewrite e.
-      intros.
-      f_equal.
-      apply proof_irrelevance.
+    destruct (Z.eq_dec (num (d d1 - d d2)) 0).
+    {
+      left.
+      rewrite num_0_iff in e.
+      apply DOred_eq.
+      rewrite DOsub_ok in e.
+      unfold Qeq in *. simpl in *.
+      lia.
     }
     right.
-    destruct d1,d2.
-    simpl in n.
-    unfold not in *.
-    intros.
+    unfold not in *. intros.
     apply n.
-    inversion H.
-    auto.
-  Qed.
+    subst.
+    rewrite num_0_iff.
+    setoid_replace 0%Q with (DO_to_Q DO0) using relation Qeq.
+    2:{ unfold DO_to_Q. unfold Qeq. auto. }
+    rewrite DOsub_ok.
+    unfold Qminus. rewrite Qplus_opp_r.
+    unfold Qeq. simpl. auto.
+  Qed. 
 
   Lemma le_not_lt: forall d1 d2 : t, (d1 <= d2)-> ~ (d2 < d1).
   Proof.
@@ -1705,15 +1801,50 @@ Module DORed.
   Lemma total_order_T : forall d1 d2 : t, {DOlt d1 d2} + {d1 = d2} + {DOlt d2 d1}.
   Proof.
     intros.
-    unfold DOlt.
-    destruct Q_dec with (DO_to_Q d1) (DO_to_Q d2).
-      destruct s; auto.
-    left.
+    destruct (DO_lt_le_dec d1 d2); auto.
+    destruct (eq_dec d1 d2); auto.
     right.
-    apply DOred_eq.
+    unfold DOlt.
+    unfold DOle in *.
+    apply Qle_lt_or_eq in d0.
+    destruct d0; auto.
+    exfalso. apply n.
+    symmetry.
+    apply DOred_eq. auto.
+  Qed. 
+
+  Lemma lt_le_dec: forall d1 d2, {d1 < d2} + {d2 <= d1}.
+  Proof. apply DO_lt_le_dec. Qed.
+
+  Definition eq_bool (d1 d2 : t) : bool := Z.eqb (num (d d1)) (num (d d2)) && Pos.eqb (den (d d1)) (den (d d2)).
+
+  Lemma eq_bool_refl: forall (d : t), eq_bool d d = true.
+  Proof.
+    intros d.
+    unfold eq_bool.
+    destruct d.  
+    simpl.
+    rewrite Z.eqb_refl.
+    rewrite Pos.eqb_refl.
     auto.
   Qed.
 
+  Lemma eq_bool_iff: forall (d1 d2 : t), eq_bool d1 d2 = true <-> d1 = d2.
+  Proof.
+    intros.
+    split; intros.
+    2: subst; apply eq_bool_refl.
+    unfold eq_bool in H.
+    apply DOred_eq_weak.
+    destruct d1. destruct d2.
+    destruct d1. destruct d0.
+    simpl in *.
+    apply andb_prop in H.
+    destruct H.
+    apply Ndec.Peqb_complete in H0.
+    apply Z.eqb_eq in H. subst. auto.
+  Qed.
+
   (* TODO: More lemmas here! *)
 End DORed.      
 
@@ -1829,17 +1960,22 @@ Proof.
   rewrite Dopp_ok.
   unfold Qminus; apply Qeq_refl.
 Qed.
-
 Definition Dle (d1 d2 : D) : Prop :=
   Qle (D_to_Q d1) (D_to_Q d2).  
 
-(*TODO: There's probably a more efficient way to implement the following:*)
 Definition Dle_bool (d1 d2 : D) : bool :=
-  Qle_bool (D_to_Q d1) (D_to_Q d2).
+  match d1,d2 with
+  | DD d1', DD d2' => DOle_bool d1' d2' 
+  | _,_ => Qle_bool (D_to_Q d1) (D_to_Q d2)
+  end.
 
 Lemma Dle_bool_iff d1 d2 : (Dle_bool d1 d2 = true) <-> Dle d1 d2.
 Proof.
   unfold Dle_bool, Dle.
+  destruct d1.
+  2: apply Qle_bool_iff.
+  destruct d2.
+   apply DOle_bool_iff.
   apply Qle_bool_iff.
 Qed.
 
@@ -1847,17 +1983,28 @@ Definition Dlt (d1 d2 : D) : Prop :=
   Qlt (D_to_Q d1) (D_to_Q d2).  
 
 Definition Dlt_bool (d1 d2 : D) : bool :=
+match d1,d2 with
+| DD d1', DD d2' => DOlt_bool d1' d2'
+| _,_ =>
   match D_to_Q d1 ?= D_to_Q d2 with
   | Lt => true
   | _ => false
-  end.
+  end
+end.
 
 Lemma Dlt_bool_iff d1 d2 : (Dlt_bool d1 d2 = true) <-> Dlt d1 d2.
 Proof.
-  unfold Dlt_bool; split.
-  destruct (Qcompare_spec (D_to_Q d1) (D_to_Q d2));
+  unfold Dlt_bool.
+  destruct d1.
+  destruct d2. apply DOlt_bool_iff.
+  split.
+  destruct (Qcompare_spec (D_to_Q (DD d)) (D_to_Q (DQ q)));
     try solve[inversion 1|auto].
   unfold Dlt; rewrite Qlt_alt; intros ->; auto.
+  split.
+  destruct (Qcompare_spec (D_to_Q (DQ q)) (D_to_Q d2));
+    try solve[inversion 1|auto].
+  unfold Dlt; rewrite Qlt_alt; intros ->; auto.  
 Qed.  
 
 Lemma Deq_dec (d1 d2 : D) : {d1=d2} + {d1<>d2}.
@@ -1934,9 +2081,6 @@ Definition Dlub (max : D) : D :=
   | DQ q => DQ (Qinv q)
   end.
 
-Eval compute in (D_to_Q (Dlub ((DD (Dmake 2 2))))).
-
-Eval compute in (Zsize 2).
 
 Local Open Scope D_scope.
 
@@ -3215,7 +3359,7 @@ Module DRed.
       rewrite <-pf1, <-pf2; apply Dred_complete; auto. }
     generalize pf1 pf2; rewrite H2; intros; f_equal; apply proof_irrelevance.
   Qed.
-  
+
   Lemma addP d1 d2 :
     D_to_Q (d (add d1 d2)) == (D_to_Q (d d1) + D_to_Q (d d2))%Q.
   Proof.
@@ -3567,17 +3711,18 @@ Module DRed.
   Proof. auto. Qed.
 
   Lemma lt_le_dec: forall d1 d2, {d1 < d2} + {d2 <= d1}.
-  Proof. intros. unfold Dle. unfold Dlt. apply Qlt_le_dec. Qed.
-
-
-  Lemma le_lt_dec: forall d1 d2,  {d1 <= d2} + {d2 < d1}.
   Proof.
-    intros.
-    unfold Dle.
-    unfold Dlt.
-    destruct Qlt_le_dec with (D_to_Q d2) (D_to_Q d1); auto.
-  Qed.
+    destruct d1; destruct d2.
+      exact (DORed.lt_le_dec d0 d1) .
+      exact (Qlt_le_dec (DO_to_Q d0) q).
+      exact (Qlt_le_dec q (DO_to_Q d0)).
+      exact (Qlt_le_dec q q0).
+  Defined.
 
+  Lemma le_lt_dec: forall d1 d2,  {d1 <= d2} + {d2 < d1}.
+  Proof. intros.
+    destruct (lt_le_dec d2 d1); auto.
+  Defined.
 
   Lemma eq_dec: forall d1 d2 : t, {d1 = d2} + {d1 <> d2}.
   Proof.
@@ -3640,6 +3785,43 @@ Module DRed.
     apply Dred_eq.
     auto.
   Qed.
+
+  Definition eq_bool (d1 d2 : t) : bool := 
+  match (d d1),(d d2) with
+  | (DD d1'), (DD d2') => DORed.eq_bool (DORed.build d1') (DORed.build d2')
+  | _ , _ => Qeq_bool (D_to_Q d1) (D_to_Q d2)
+  end.
+
+  Lemma eq_bool_refl: forall (d : t), eq_bool d d = true.
+  Proof.
+    intros d.
+    unfold eq_bool.
+    destruct d.  
+    simpl.
+    destruct d0.
+      apply DORed.eq_bool_refl.
+    apply Qeq_bool_refl.
+  Qed.
+
+  Lemma eq_bool_iff: forall (d1 d2 : t), eq_bool d1 d2 = true <-> d1 = d2.
+  Proof.
+    intros.
+    split; intros.
+    2: subst; apply eq_bool_refl.
+    unfold eq_bool in H.
+    destruct d1. destruct d0; simpl in *.
+    2:{ apply Qeq_bool_iff in H. apply Dred_eq. auto. }
+    destruct d2. destruct d1; simpl in *.
+    2:{ apply Qeq_bool_iff in H. apply Dred_eq. auto. }
+    apply DORed.eq_bool_iff in H.
+    unfold DORed.build in H.
+    inversion H.
+    apply Dred_eq.
+    simpl.
+    apply DOred_complete_converse.
+    auto.
+  Qed.
+
   (* TODO: More lemmas here! *)
 End DRed.      
 
diff --git a/enumerables.v b/enumerables.v
index e9c2790..4aa3d2f 100644
--- a/enumerables.v
+++ b/enumerables.v
@@ -19,11 +19,33 @@ Require Import OUVerT.compile.
   player indices, represented as positive.*)
 Require Import Coq.FSets.FMapAVL Coq.FSets.FMapFacts.
 Require Import Structures.Orders NArith.
+Require Import Permutation.
 
 
+Lemma NoDupA_NoDup: forall T (l : list T), NoDupA (fun x : T => [eta eq x]) l <-> NoDup l.
+Proof.
+  intros.
+  split;intros.
+  {
+    induction H. constructor.
+    constructor; auto.
+    unfold not. intros.
+    apply H.
+    apply In_InA; auto.
+  }
+  induction H. constructor.
+  constructor; auto.
+  unfold not. intros.
+  apply H. 
+  apply InA_alt in H1. 
+  destruct H1.
+  destruct H1.
+  subst. auto.
+Qed.
 
 Module Enum_table.
 
+
   Definition nonempty_head (T : Type) (l : list T) (H : O <> length l) : T.
     destruct l eqn:e.
       exfalso. apply H. auto.
@@ -135,6 +157,7 @@ Module Enum_table.
   Section eqb_proofs.
     Variable T : Type.
     Hypothesis eqb: forall (t1 t2 : T), {t1 = t2} + {t1 <> t2}.
+    
 
     Lemma nth_index_of_eqb: forall (l : list T) (t1 t2 : T),
       In t1 l -> nth (index_of l (eqb t1)) l t2 = t1.
@@ -190,14 +213,206 @@ Module Enum_table.
       apply lt_S_n; auto.
     Qed.
 
+    Lemma list_nth_eq: forall (A : Type) (a1 a2 : A) (l1 l2: list A), length l1 = length l2 -> (forall (n : nat), (n < length l1)%coq_nat -> nth n l1 a1 = nth n l2 a2) ->
+          l1 = l2.
+    Proof.
+      intros.
+      generalize dependent l2.
+      induction l1; intros.
+        destruct l2; auto. inversion H.
+      destruct l2.
+        inversion H.
+      f_equal.
+      {
+        assert(a = nth 0 (a :: l1) a1). auto.
+        assert(a0 = nth 0 (a0 :: l2) a2). auto.
+        rewrite H2. rewrite H1. apply H0.
+        simpl. apply Nat.lt_0_succ.
+      }
+      apply IHl1.
+        inversion H. auto.
+      intros.
+      assert(nth (S n) (a :: l1) a1 = nth (S n) (a0 :: l2) a2); auto.
+      apply H0. simpl. apply lt_n_S. auto.
+  Qed.
+
   (**Lemma reflet_eqType_eqb: forall (T : eqType) (x y : T), reflect (x=y) (eqType_eqb x y).
   Proof.
     intros.
     destruct (eqType_eqb x y) eqn:e; auto.
     { constructor. apply eqType_eqb_true_iff. auto. }
     constructor. apply eqType_eqb_false_iff. auto.
-  Qed.**)
+  Qed.**) 
+
+  Lemma index_of_n: forall (l : list T) (x : T), index_of l (eqb x) <> length l -> In x l.
+  Proof. 
+    intros.
+    induction l.
+      simpl in *. exfalso. auto.
+    simpl in *.
+    destruct (eqb a x); auto.
+    right.
+    apply IHl.
+    destruct (eqb x a); auto.
+    simpl in *.
+    rewrite -> Nat.succ_inj_wd_neg in H.
+    auto.
+  Qed.
+
+  Lemma total_exists_index: forall (l : list T), 
+      NoDup l -> (forall n : nat, (n < length l)%coq_nat -> exists a : T, index_of l (eqb a) = n).
+  Proof.
+    intros.
+    generalize dependent n.
+    induction l; intros.
+     inversion H0.
+    simpl.
+    inversion H.
+    subst.
+    destruct n.
+      exists a. rewrite eqb_refl. auto.
+    simpl in H0.
+    destruct IHl with n; auto.
+      apply lt_S_n. auto.
+    destruct n.
+    {
+      destruct l.
+        simpl in H0. inversion H0. inversion H5.
+      inversion H4.
+      subst.      
+      simpl.
+      exists t.
+      destruct (eqb t a).
+        exfalso. apply H3. simpl. auto.
+      simpl. rewrite eqb_refl. auto.
+    }
+    assert(In x l).
+      apply index_of_n. rewrite H1. apply Nat.lt_neq. apply lt_S_n. auto.
+    exists x.
+    destruct (eqb x a).
+      subst. exfalso. auto.
+    simpl. rewrite H1. auto.
+  Qed.
+
+  Lemma enum_ok_nth_lookup_ext: forall (T2 : Type) (t1_enum : list T) (l1 l2 : list T2) (x y: T2),
+      length l1 = length t1_enum -> length l2 = length t1_enum ->
+      @Enum_ok T t1_enum -> (forall t, nth (index_of t1_enum (eqb t)) l1 x = nth (index_of t1_enum (eqb t)) l2 y) ->
+      l1 = l2.
+  Proof.  
+    intros.
+    apply list_nth_eq with x y.
+      rewrite H. auto.
+    intros.
+    assert(exists t1 : T, index_of t1_enum (eqb t1) = n).
+      apply total_exists_index. inversion H1. rewrite <- NoDupA_NoDup.  auto.
+      rewrite <- H. auto.    
+    destruct H4.
+    rewrite <- H4.
+    apply H2.
+  Qed.
+
+  Lemma not_In_index_of_length: forall x l, ~ In x l <-> length l = index_of l (eqb x).
+  Proof.
+    intros.
+    split; intros.
+    {
+      generalize dependent x.
+      induction l; intros; auto.
+      simpl.
+      destruct (eqb x a). subst.
+        exfalso. apply H. simpl. auto.
+      simpl.
+      f_equal.
+      apply IHl.
+      unfold not. intros.
+      apply H. simpl. auto.
+    }
+    unfold not.
+    intros.
+    generalize dependent x.
+    induction l; simpl. auto.
+    intros.
+    destruct H0.
+    {
+      subst.
+      destruct (eqb x x); auto. inversion H.
+    }
+    destruct (eqb x a); simpl in H. inversion H.
+    inversion H.
+    apply IHl with x; auto.
+  Qed.
+
+
   End eqb_proofs.
+  Class lookup_table (table_t key_t value_t : Type) := {
+    from_func : (key_t -> value_t) -> table_t; 
+    table_update : table_t -> key_t -> value_t -> table_t;
+    table_lookup : table_t -> key_t -> value_t;
+    table_lookup_from_func: forall f k, table_lookup (from_func f) k = f k;
+    table_lookup_update: forall t k v, table_lookup (table_update t k v) k = v; 
+    table_lookup_update_neq: forall t k1 k2 v, k1 <> k2 -> table_lookup (table_update t k1 v) k2 = table_lookup t k2;
+  }.
+
+  Lemma map_zip_fst: forall T1 T2 (l1 : list T1) (l2 : list T2), (length l1 <= length l2)%nat -> l1 = map fst (zip l1 l2).
+  Proof.
+    intros.
+    generalize dependent l1.
+    induction l2; intros. destruct l1; auto. inversion H.
+    simpl in *.
+    destruct l1; auto.
+    simpl.
+    f_equal.
+    apply IHl2.
+    inversion H. auto.
+  Qed.
+    
+
+  Lemma map_zip_snd: forall T1 T2 (l1 : list T1) (l2 : list T2), (length l2 <= length l1)%nat -> l2 = map snd (zip l1 l2).
+  Proof.
+    intros.
+    generalize dependent l1.
+    induction l2; intros. simpl. destruct l1; auto.
+    simpl.
+    destruct l1. inversion H.
+    simpl. f_equal.
+    apply IHl2.
+    auto.
+  Qed. 
+
+  Lemma index_of_lt_length: forall T (f : T->bool) l, (index_of l f < length l)%coq_nat <-> 
+      (exists x, In x l /\ f x).
+  Proof.
+    intros.
+    split.
+    {
+      intros.
+      induction l.
+        inversion H.
+      simpl in H.
+      destruct (f a) eqn:e.
+        exists a. split; simpl; auto.
+      destruct IHl.
+        apply lt_S_n. auto.
+      simpl.
+      destruct H0. eauto.
+    }
+    induction l; intros.
+      destruct H. destruct H. inversion H.
+    simpl.
+    destruct H.
+    destruct H.
+    simpl in H.
+    destruct H. subst. rewrite H0.
+      apply Nat.lt_0_succ.
+    destruct (f a).
+      apply Nat.lt_0_succ.
+    apply lt_n_S.
+    apply IHl.
+    eauto.
+  Qed.
+
+
+
   Section enum_table.
 
     Variable T1 : Type.
@@ -227,7 +442,20 @@ Module Enum_table.
 
     Definition eq_func (t : table) (f : T1->T2):= forall (x : T1), lookup t x = f x.
 
-    Definition to_func (t : table) : (T1->T2) := (fun x => lookup t x).
+    Definition to_func (t : table) : (T1->T2) := lookup t.
+
+   Program Definition update (t : table) (k : T1) (v : T2) : table :=
+      @table_mk (map (fun kv => if T1_eqdec k (fst kv) then v else (snd kv))  (zip_table t)) _.
+    Next Obligation.
+      rewrite map_length.
+      unfold zip_table.
+      repeat rewrite length_size_eq.
+      rewrite size_zip.
+      repeat rewrite <- length_size_eq.
+      repeat rewrite (t_list_length t).
+      rewrite minnn. auto.
+    Qed.
+
 
     Lemma zip_table_length: forall (t : table), length (zip_table t) = length T1_enum.
     Proof.
@@ -283,7 +511,7 @@ Module Enum_table.
       destruct T1_enum_ok. auto.
     Qed. 
 
-    Lemma zip_table_map: forall (f : T1->T2), zip_table (map_to_table f) = map (fun x => (x, f x)) T1_enum.
+    Lemma zip_table_map_to_table: forall (f : T1->T2), zip_table (map_to_table f) = map (fun x => (x, f x)) T1_enum.
     Proof. 
       intros.
       unfold map_to_table. unfold zip_table. simpl.
@@ -298,11 +526,159 @@ Module Enum_table.
       generalize dependent (map_to_table_obligation_1 f1).
       rewrite -> H.
       intros. f_equal. apply proof_irrelevance.
-    Qed.      
+    Qed.
+    
+    Lemma t_list_eq: forall t1 t2, t_list t1 = t_list t2 -> t1 = t2.
+    Proof.
+      intros.
+      destruct t1.
+      destruct t2.
+      generalize t_list_length1.
+      simpl in H.
+      rewrite <- H.
+      intros.
+      f_equal.
+      apply proof_irrelevance.
+    Qed.
+
+   Lemma table_eq_ext: forall t1 t2,(lookup t1) =1 (lookup t2) -> t1 = t2.
+   Proof.
+      intros.
+      destruct t1.
+      destruct t2.
+      apply t_list_eq.
+      simpl.
+      eapply (@enum_ok_nth_lookup_ext T1 T1_eqdec T2 T1_enum t_list0 t_list1 (table_head {| t_list := t_list0; t_list_length := t_list_length0 |}) _ _); auto.
+      intros.
+      unfold lookup in H. unfold eqfun in H. simpl in H.
+      rewrite H.
+      f_equal.
+      Unshelve. auto.
+    Qed.
+    
+    (*Lemma zip_table_ext: forall t1 t2, zip_table t1 = zip_table t2 -> t1 = t2.
+    Proof. Admitted.
+*)
+    Lemma t_list_zip_table_snd: forall t, t_list t = map snd (zip_table t).
+    Proof.
+      intros.
+      unfold zip_table.
+      rewrite <- map_zip_snd. auto.
+      rewrite (t_list_length t). auto.
+    Qed.
+
+    Lemma T1_eqdec_refl: forall x, T1_eqdec x x.
+    Proof.
+      intros.
+      destruct(T1_eqdec x x); auto.
+    Qed.
+
+    Lemma map_lookup: forall t, map (lookup t) T1_enum = t_list t.
+    Proof.
+      intros.
+      unfold lookup.
+      inversion T1_enum_ok.
+      clear T1_enum_ok.
+      unfold enumerable_fun in enum_nodup.
+      generalize (table_head t).
+      assert(length T1_enum = length (t_list t)).
+        rewrite <- t_list_length. auto.
+      generalize (t_list t) H.
+      clear H t. clear enum_total.
+      clear T1_enum_ne.
+      induction T1_enum as [|eh].
+        intros. simpl in *. symmetry. apply length_zero_iff_nil. auto.
+      intros l H A1.
+      simpl in *.
+      rewrite T1_eqdec_refl.
+      destruct l as [|lh].
+        inversion H.
+      simpl.
+      f_equal. 
+      destruct IHe with l A1; auto.
+        simpl in *. inversion enum_nodup. auto.
+      apply map_ext_in.
+      intros x hIn.
+      inversion H.
+      clear H.
+      inversion enum_nodup. subst.
+      destruct (T1_eqdec x eh); subst; simpl.
+        exfalso. apply H2. apply In_InA; auto.
+      f_equal.
+      apply IHe.
+        inversion enum_nodup; auto.
+      auto.
+    Qed.
+
+    Lemma zip_table_map: forall t, zip_table t = map (fun x => (x,lookup t x)) T1_enum.
+    Proof.  
+      intros.
+      unfold zip_table.
+      rewrite <- map_lookup.
+      rewrite zip_map. auto.
+    Qed.
+
+
+    
+      
+    Lemma map_to_table_lookup : forall (t : table), map_to_table (lookup t) = t.
+    Proof.
+      intros.
+      apply table_eq_ext.
+      unfold eqfun. intros.
+      rewrite lookup_map. auto.
+    Qed.
+
+    
+    Lemma update_map_to_table: forall t k v, update t k v = (map_to_table (fun k' => if T1_eqdec k k' then v else (lookup t k'))).
+    Proof.
+      intros.
+      unfold update.
+      unfold map_to_table.
+      apply t_list_eq.
+      simpl.
+      rewrite zip_table_map.
+      rewrite map_map. auto.
+    Qed.
+      
+
+    Lemma lookup_update: forall t k v, lookup (update t k v) k = v.
+    Proof.
+      intros.
+      rewrite update_map_to_table.
+      rewrite lookup_map.
+      rewrite T1_eqdec_refl. auto.
+    Qed.
+
+
+    Lemma lookup_update_neq: forall t k1 k2 v, k1 <> k2 -> lookup (update t k1 v) k2 = lookup t k2.
+    Proof.
+      intros.
+      rewrite update_map_to_table.
+      rewrite lookup_map.
+      destruct (T1_eqdec k1 k2); auto.
+      exfalso. auto.
+    Qed.
+    
+
+    Instance table_lookup_table : lookup_table table T1 T2 :=
+      @Build_lookup_table table T1 T2 map_to_table update lookup lookup_map lookup_update lookup_update_neq.
       
 
   End enum_table.
 
+ (*  Section enum_tree.
+    Variable T1 : Type.
+    Variable T2 : Type.
+    Variable T1_enum : Enumerable T1.
+    Variable T1_enum_ok : @Enum_ok T1 T1_enum.
+    Variable T1_enum_ne : O <> length T1_enum.
+    Variable T1_eqdec : forall t1 t2 : T1, {t1 = t2} + {t1 <> t2}.
+    Variable comp : T1 -> T1 -> bool.
+
+  End enum_tree. *)
+
+
 
   Definition table_eqb (T1 T2 : eqType) (T1_enum : Enumerable T1) (t1 t2 : table T2 T1_enum) : bool := 
    eq_op (t_list t1) (t_list t2).
@@ -1029,3 +1405,159 @@ Proof.
   rewrite <- H2.
   apply IHn.
 Qed.
+
+
+Lemma In_InA: forall (T : Type) (l : list T) (x : T), In x l <-> InA  (fun x => [eta eq x]) x l.
+Proof.
+  intros.
+  split; intros.
+  {
+    induction l.
+      inversion H.
+    simpl in H. destruct H; auto.
+  }
+  induction H; simpl; auto.
+Qed.
+
+Lemma NoDup_NoDupA: forall (T : Type) (l : list T), NoDup l <-> NoDupA (fun x => [eta eq x]) l.
+Proof.
+  intros.
+  split; intros.
+  {
+    induction H; auto.
+    constructor; auto.
+    rewrite <- In_InA. auto.
+  }
+  induction H; constructor; auto.
+  rewrite In_InA. auto.
+Qed.
+
+Lemma Enumerable_nodup_list_diff: forall (T : Type) (enum: Enumerable T) (l : list T), 
+   @Enum_ok T enum -> NoDup l -> exists l' : list T, Permutation (enumerate T) (app l l').
+Proof.
+  intros.
+  induction l.
+    exists (enumerate T). simpl. apply Permutation_refl.
+  inversion H0.
+  subst.
+  apply IHl in H4.
+  destruct H4 as [l2].
+  destruct (Add_inv a l2) as [l3].
+  {
+    assert(In a (l ++ l2)). 
+      eapply Permutation_in. apply H1. apply enum_total.
+    apply in_app_or in H2.
+    destruct H2; auto.
+    exfalso. apply H3. auto.
+  }
+  exists l3.  
+  simpl.
+  apply Permutation_sym.
+  eapply perm_trans.
+  apply Permutation_middle.
+  eapply perm_trans.
+  2:{ apply Permutation_sym. apply H1. }
+  apply Permutation_app.
+    apply Permutation_refl.
+  apply Permutation_Add. auto.
+Qed.
+
+
+Record enum_subset (T : Type) (l : list T) : Type :=
+  mk_enum_subset {
+    enum_subset_element : T;
+    enum_subset_In : List.In enum_subset_element l
+  }.
+
+Definition enum_subset_eq_dec T (l : list T) (eqdec : forall x y : T, {x=y} + {x<>y}) (x y : enum_subset l) : {x = y} + {x <> y}.
+  destruct x as [x Hx].
+  destruct y as [y Hy].
+  destruct (eqdec x y). subst.
+    left. f_equal. apply proof_irrelevance.
+  right.
+  unfold not. intros.
+  inversion H.
+  subst. auto.
+Defined.
+
+Program Fixpoint enum_subset_enumerate (T : Type) (l : list T) : @Enumerable (@enum_subset T l) :=
+match l with
+| nil => nil
+| x :: l' => (@mk_enum_subset T l x _) :: 
+    (map (fun a => @mk_enum_subset T (x :: l') (enum_subset_element a) _)
+      (@enum_subset_enumerate T l'))
+end.
+Next Obligation.
+  simpl. auto.
+Qed.
+Next Obligation.
+  right.
+  apply enum_subset_In.
+Qed.
+
+Lemma enum_subset_list: forall T (l : list T), (map (fun x => enum_subset_element x) (enum_subset_enumerate l)) = l.
+Proof.
+  intros.
+  induction l; auto.
+  simpl.
+  f_equal.
+  rewrite map_map.
+  simpl.
+  auto.
+Qed.
+
+
+Lemma enum_subset_ok: forall {T : Type} (l : list T) (H : NoDupA (fun x : T => [eta eq x]) l) (*eq_dec : forall x y : T, {x=y}+{x<>y}*), 
+      @Enum_ok (@enum_subset T l) (@enum_subset_enumerate T l).
+Proof.
+  intros.
+  constructor.
+  {
+    unfold enumerable_fun.
+    induction H. simpl. auto.
+    simpl. 
+    constructor.
+    {
+      unfold not.
+      intros.
+      apply H.
+      rewrite <- In_InA.
+      rewrite <- In_InA in H1.
+      apply (in_map (fun x =>  enum_subset_element x) ) in H1.
+      rewrite map_map in H1.
+      simpl in H1.
+      rewrite enum_subset_list in H1. auto.
+    }
+    apply NoDupA_map; auto.
+    intros.
+    destruct x0.
+    destruct y.
+    simpl in *.
+    inversion H1.
+    subst.
+    f_equal.
+    apply proof_irrelevance.
+  }
+  intros.
+  clear H.
+  unfold enumerable_fun.
+  induction l.
+    destruct a. inversion enum_subset_In0.
+  simpl.
+  destruct a.
+  simpl in *.
+  destruct enum_subset_In0; subst.
+    left. f_equal. apply proof_irrelevance.
+  right.
+  specialize (IHl ({| enum_subset_element := enum_subset_element0; enum_subset_In := i |})).
+  apply in_map_iff.
+  eexists ({|
+  enum_subset_element := enum_subset_element0;
+  enum_subset_In := _ |}).
+  split.
+  {
+    f_equal.
+    apply proof_irrelevance.
+  }
+  apply IHl.
+Qed.
diff --git a/extrema.v b/extrema.v
index ddaaea0..c5a7ba3 100644
--- a/extrema.v
+++ b/extrema.v
@@ -1891,7 +1891,7 @@ Module num_Extrema.
   End use_Numerics.
   Section use_Numerics2.
 
-  Context (Nt:Type) `{Numeric_Props Nt}.
+  Context (Nt:Type) `{Numeric_Props Nt} `{Nt_R_inj : @Numeric_R_inj Nt numeric_t}.
 
   
    
diff --git a/generalized_bigops.v b/generalized_bigops.v
index 86a362c..efc7288 100644
--- a/generalized_bigops.v
+++ b/generalized_bigops.v
@@ -10,6 +10,8 @@ From mathcomp Require Import all_algebra.
 
 Require Import OUVerT.numerics.
 Require Import OUVerT.extrema.
+Require Import OUVerT.compile.
+Require Import OUVerT.enumerables.
 
 Delimit Scope R_scope with R.
 
@@ -392,7 +394,7 @@ Proof.
   auto.
 Qed.
 
-
+  
 End use_numeric_props.
 
 
@@ -677,6 +679,7 @@ Proof.
   apply: big_sum_ge0 => x; rewrite mem_filter; case/andP => Hx Hy; apply: H1 => //.
 Qed.  
 
+
 Lemma big_sum_pred (T:eqType) (cs:seq T) (f:T -> Nt) (p:pred T) :
   big_sum cs (fun t => if p t then f t else Numerics.plus_id) =
   big_sum [seq t <- cs | p t] f.
@@ -797,23 +800,7 @@ Proof.
   apply Numerics.plus_comm.
 Qed.
 
-Lemma to_R_big_sum T (cs : seq T) (f : T -> Nt): (big_sum cs (fun x => Numerics.to_R (f x))) = Numerics.to_R (big_sum cs f).
-Proof.
-  induction cs; simpl.
-    rewrite Numerics.to_R_plus_id. auto.
-  rewrite IHcs.
-  rewrite Numerics.to_R_plus.
-  auto.
-Qed.
 
-Lemma to_R_big_product T (cs : seq T) (f : T -> Nt): (big_product cs (fun x => Numerics.to_R (f x))) = Numerics.to_R (big_product cs f).
-Proof.
-  induction cs; simpl.
-    rewrite Numerics.to_R_mult_id. auto.
-  rewrite IHcs.
-  rewrite Numerics.to_R_mult.
-  auto.
-Qed.
 
 
 Lemma big_sum_filter: forall (T : Type) (cs : seq T) (f : T->Nt) (g : T->bool),
@@ -830,6 +817,26 @@ Proof.
   apply IHcs.
 Qed.
 
+  Section use_Numeric_R_inj.
+    Context `{Nt_R_inj : @Numerics.Numeric_R_inj Nt numeric_t}.
+  Lemma to_R_big_sum T (cs : seq T) (f : T -> Nt): (big_sum cs (fun x => Numerics.to_R (f x))) = Numerics.to_R (big_sum cs f).
+  Proof.
+  induction cs; simpl.
+    rewrite Numerics.to_R_plus_id. auto.
+  rewrite IHcs.
+  rewrite Numerics.to_R_plus.
+  auto.
+Qed.
+
+Lemma to_R_big_product T (cs : seq T) (f : T -> Nt): (big_product cs (fun x => Numerics.to_R (f x))) = Numerics.to_R (big_product cs f).
+Proof.
+  induction cs; simpl.
+    rewrite Numerics.to_R_mult_id. auto.
+  rewrite IHcs.
+  rewrite Numerics.to_R_mult.
+  auto.
+Qed.
+End use_Numeric_R_inj.
 
 End use_Numeric2.
 
diff --git a/numerics.v b/numerics.v
index f1bb555..1fce052 100644
--- a/numerics.v
+++ b/numerics.v
@@ -52,7 +52,7 @@ Module Numerics.
         neg : T->T where "- n" := (neg n) : Num;
         mult: T -> T -> T where "n * m" := (mult n m) : Num;
         pow_nat: T -> nat -> T;
-        to_R : T -> R;
+        
 
         of_nat: nat -> T;
         plus_id: T;
@@ -98,19 +98,24 @@ Module Numerics.
         pow_natO: forall t, pow_nat t O = mult_id;
         pow_nat_rec: forall t n, pow_nat t (S n) = t * pow_nat t n;
 
-        to_R_plus: forall t1 t2 : T, Rplus (to_R t1) (to_R t2) = to_R (t1 + t2);
-        to_R_mult: forall t1 t2 : T, Rmult (to_R t1) (to_R t2) = to_R (t1 * t2);
-        to_R_lt: forall t1 t2 : T, t1 < t2 <-> Rlt (to_R t1) (to_R t2);
-        to_R_neg: forall t : T, Ropp (to_R t) = to_R (- t);
-        to_R_inj: forall n m : T, to_R n = to_R m -> n = m;
-      
         total_order_T : forall r1 r2, {r1 < r2} + {r1 = r2} + {r2 < r1};
 
         eqb_true_iff: forall n m, eqb n m <-> n = m;
         ltb_true_iff: forall n m, ltb n m <-> n < m;
 
       }.
-      Ltac to_R_distr := 
+  Class Numeric_R_inj (T : Type) `{numeric_t : Numeric T} :=
+  mkNumericRInj {
+    to_R : T -> R;
+    to_R_plus: forall t1 t2 : T, Rplus (to_R t1) (to_R t2) = to_R (t1 + t2);
+    to_R_mult: forall t1 t2 : T, Rmult (to_R t1) (to_R t2) = to_R (t1 * t2);
+    to_R_lt: forall t1 t2 : T, t1 < t2 <-> Rlt (to_R t1) (to_R t2);
+    to_R_neg: forall t : T, Ropp (to_R t) = to_R (- t);
+    to_R_inj: forall n m : T, to_R n = to_R m -> n = m;
+  }.
+
+
+  Ltac to_R_distr := 
     repeat (
       try (rewrite <- to_R_mult);
       try (rewrite <- to_R_plus);
@@ -138,7 +143,6 @@ Module Numerics.
 
     Definition minus (n m : Nt) := n + - m.
 
-
     Context  `{NtProps : Numeric_Props (numeric_t := H) Nt}.
 
     Lemma eqb_false_iff: forall n m, eqb n m = false <-> n <> m.
@@ -154,6 +158,7 @@ Module Numerics.
       exfalso.
       by apply eqb_true_iff in e.
     Qed.
+
       
 
     Lemma ltb_false_iff: forall n m, ltb n m = false <-> ~ n < m.
@@ -189,6 +194,7 @@ Module Numerics.
       auto.
     Qed.
 
+
     Program Definition numeric_ring :=  @mk_rt Nt plus_id mult_id plus mult minus neg eq plus_id_l 
       plus_comm plus_assoc mult_id_l mult_comm mult_assoc _ _ plus_neg_r.
     Next Obligation.
@@ -206,7 +212,6 @@ Module Numerics.
       apply H1. auto.
     Qed.
 
-
     Lemma plus_assoc_reverse : forall r1 r2 r3, r1 + r2 + r3 = r1 + (r2 + r3).
     Proof. intros. rewrite plus_assoc. auto. Qed.
 
@@ -222,6 +227,7 @@ Module Numerics.
       auto.
     Qed.
 
+
     Lemma eq_dec: forall t1 t2 : Nt, {t1 = t2} + {t1 <> t2}.
     Proof.
       intros.
@@ -1118,25 +1124,6 @@ Module Numerics.
     auto.
   Qed.
 
-  Lemma to_R_plus_id: to_R 0 = IZR Z0.
-  Proof.
-    rewrite <- Rplus_opp_r with (to_R 0).
-    rewrite to_R_neg.
-    rewrite to_R_plus.
-    rewrite plus_id_l.
-    rewrite neg_plus_id.
-    auto.
-  Qed.
-
-  Lemma to_R_neq: forall n m : Nt, n <> m <-> to_R n <> to_R m.
-  Proof.
-    intros.
-    split; unfold not; intros.
-      apply H0. apply to_R_inj. auto.
-    apply H0.
-    rewrite H1.
-    auto.
-  Qed.    
       
 
   Lemma plus_id_neq_mult_id: 0 <> 1.
@@ -1160,6 +1147,144 @@ Module Numerics.
     auto.
   Qed.
 
+  Lemma leb_ltb_or_eqb: forall t1 t2 : Nt, leb t1 t2 = ltb t1 t2 || eqb t1 t2.
+  Proof.
+    intros.
+    destruct (leb t1 t2) eqn:e.
+    {
+      apply leb_true_iff in e.
+      destruct e.
+      { apply ltb_true_iff in H0. rewrite H0. auto. }
+      rewrite H0.
+      rewrite eqb_refl.      
+      rewrite orb_true_r.
+      auto.
+    }
+    apply leb_false_iff in e.
+    assert (ltb t1 t2 = false).
+      apply ltb_false_iff. unfold not. intros. apply le_lt_weak in H0. auto.
+    rewrite H0.
+    apply not_le_lt in e.
+    apply lt_not_eq in e.
+    apply eqb_false_iff in e.
+    rewrite eqb_symm.
+    rewrite e.
+    auto.
+  Qed.
+
+  
+  Lemma pow_nat_ge1_le: forall x n m,  1 <= x -> Nat.le n m -> pow_nat x n <= pow_nat x m.
+  Proof. 
+    intros.
+    assert(forall m', pow_nat x n <=  pow_nat x (n+m')).
+    { 
+      intros. induction m'. rewrite addn0. auto.
+      rewrite addnS.
+      rewrite <- mult_id_l with (pow_nat x n).
+      rewrite pow_nat_rec.
+      apply mult_le_compat; auto.
+        apply le_lt_weak. apply plus_id_lt_mult_id.
+      apply pow_ge_0.
+      apply le_trans with 1; auto.
+      apply le_lt_weak. apply plus_id_lt_mult_id.
+    }
+    destruct Nat_le_exists_diff with n m; auto.
+    rewrite <- H3.
+    apply H2.
+  Qed.
+
+  Lemma pow_nat_le1_le: forall x n m, 0 < x -> x <= 1 -> Nat.le n m -> pow_nat x m <= pow_nat x n.
+  Proof. 
+    intros.
+    assert(forall m', pow_nat x (n+m') <=  pow_nat x n).
+    { 
+      intros. induction m'. rewrite addn0. auto.
+      rewrite addnS.
+      rewrite <- mult_id_l with (pow_nat x n).
+      rewrite pow_nat_rec.
+      apply mult_le_compat; auto.
+      apply pow_ge_0. auto.
+    }
+    destruct Nat_le_exists_diff with n m; auto.
+    rewrite <- H4.
+    apply H3.
+  Qed.
+
+  Lemma lt_diff_pos: forall x y : Nt, x < y -> 0 < (y + - x).
+  Proof. 
+    intros.
+    rewrite <- plus_neg_r with x.
+    apply plus_lt_compat_r. auto.
+  Qed. 
+
+  Lemma min_comm: forall x y : Nt, min x y = min y x.
+  Proof. 
+    intros. unfold min.
+    destruct (total_order_T x y).
+    {
+      destruct s.
+      2: { rewrite e. auto. }
+      assert(leb y x = false).
+        apply leb_false_iff. apply lt_not_le. auto.
+      rewrite H0.
+      apply le_lt_weak in l.
+      apply leb_true_iff in l. rewrite l. auto.
+    }
+    assert(leb x y = false).
+    { apply leb_false_iff. apply lt_not_le. auto. }
+    rewrite H0. apply le_lt_weak in l. apply leb_true_iff in l. rewrite l. auto.
+  Qed.
+
+  Lemma ge_min_l: forall x y : Nt, min x y <= x.
+  Proof. 
+    intros.
+    unfold min. 
+    destruct (total_order_T x y).
+    {
+      destruct s.
+      2:{  rewrite e. destruct (leb y y); auto. }
+      apply le_lt_weak in l.
+      apply leb_true_iff in l. rewrite l. auto.
+    }
+    apply le_lt_weak.
+    apply le_lt_trans with y; auto.
+    apply lt_not_le in l. apply leb_false_iff in l.
+    rewrite l. auto.
+  Qed.
+
+  Lemma ge_min_r: forall x y : Nt, min x y <= y.
+  Proof. intros. rewrite min_comm. apply ge_min_l. Qed.
+
+  Lemma min_id: forall x : Nt, min x x = x.
+  Proof. intros. unfold min. destruct (leb x x); auto. Qed.
+
+  Lemma min_cases: forall x y : Nt, min x y = x \/ min x y = y.
+  Proof. intros. unfold min. destruct (leb x y); auto. Qed.
+
+  Section use_numeric_R_inj.
+    Context {NtRInj : @Numeric_R_inj Nt H}.
+
+  Lemma to_R_plus_id: to_R 0 = IZR Z0.
+  Proof.
+    rewrite <- Rplus_opp_r with (to_R 0).
+    rewrite to_R_neg.
+    rewrite to_R_plus.
+    rewrite plus_id_l.
+    rewrite neg_plus_id.
+    auto.
+  Qed.
+
+  Lemma to_R_neq: forall n m : Nt, n <> m <-> to_R n <> to_R m.
+  Proof.
+    intros.
+    split; unfold not; intros.
+      apply H0. apply to_R_inj. auto.
+    apply H0.
+    rewrite H1.
+    auto.
+  Qed.    
+
+
   Lemma to_R_mult_id: to_R 1 = IZR (Zpos xH).
   Proof.
     assert( forall x y : R, Rmult x y = x -> x = IZR Z0 \/ y = IZR (Zpos xH)).
@@ -1456,33 +1581,6 @@ Module Numerics.
       unfold not; intros; apply H0; apply to_R_le; auto.
   Qed.
 
-  
-
-  Lemma leb_ltb_or_eqb: forall t1 t2 : Nt, leb t1 t2 = ltb t1 t2 || eqb t1 t2.
-  Proof.
-    intros.
-    destruct (leb t1 t2) eqn:e.
-    {
-      apply leb_true_iff in e.
-      destruct e.
-      { apply ltb_true_iff in H0. rewrite H0. auto. }
-      rewrite H0.
-      rewrite eqb_refl.      
-      rewrite orb_true_r.
-      auto.
-    }
-    apply leb_false_iff in e.
-    assert (ltb t1 t2 = false).
-      apply ltb_false_iff. unfold not. intros. apply le_lt_weak in H0. auto.
-    rewrite H0.
-    apply not_le_lt in e.
-    apply lt_not_eq in e.
-    apply eqb_false_iff in e.
-    rewrite eqb_symm.
-    rewrite e.
-    auto.
-  Qed.
-
   Lemma to_R_abs: forall n : Nt, to_R (abs n) = Rabs (to_R n).
   Proof.
     intros.
@@ -1518,99 +1616,26 @@ Module Numerics.
     rewrite IHn.
     auto.
   Qed.
+  End use_numeric_R_inj.
 
-  Lemma pow_nat_ge1_le: forall x n m,  1 <= x -> Nat.le n m -> pow_nat x n <= pow_nat x m.
-  Proof. 
-    intros.
-    assert(forall m', pow_nat x n <=  pow_nat x (n+m')).
-    { 
-      intros. induction m'. rewrite addn0. auto.
-      rewrite addnS.
-      rewrite <- mult_id_l with (pow_nat x n).
-      rewrite pow_nat_rec.
-      apply mult_le_compat; auto.
-        apply le_lt_weak. apply plus_id_lt_mult_id.
-      apply pow_ge_0.
-      apply le_trans with 1; auto.
-      apply le_lt_weak. apply plus_id_lt_mult_id.
-    }
-    destruct Nat_le_exists_diff with n m; auto.
-    rewrite <- H3.
-    apply H2.
-  Qed.
-
-  Lemma pow_nat_le1_le: forall x n m, 0 < x -> x <= 1 -> Nat.le n m -> pow_nat x m <= pow_nat x n.
-  Proof. 
-    intros.
-    assert(forall m', pow_nat x (n+m') <=  pow_nat x n).
-    { 
-      intros. induction m'. rewrite addn0. auto.
-      rewrite addnS.
-      rewrite <- mult_id_l with (pow_nat x n).
-      rewrite pow_nat_rec.
-      apply mult_le_compat; auto.
-      apply pow_ge_0. auto.
-    }
-    destruct Nat_le_exists_diff with n m; auto.
-    rewrite <- H4.
-    apply H3.
-  Qed.
-
-  Lemma lt_diff_pos: forall x y : Nt, x < y -> 0 < (y + - x).
-  Proof. 
-    intros.
-    rewrite <- plus_neg_r with x.
-    apply plus_lt_compat_r. auto.
-  Qed. 
-
-  Lemma min_comm: forall x y : Nt, min x y = min y x.
-  Proof. 
-    intros. unfold min.
-    destruct (total_order_T x y).
-    {
-      destruct s.
-      2: { rewrite e. auto. }
-      assert(leb y x = false).
-        apply leb_false_iff. apply lt_not_le. auto.
-      rewrite H0.
-      apply le_lt_weak in l.
-      apply leb_true_iff in l. rewrite l. auto.
-    }
-    assert(leb x y = false).
-    { apply leb_false_iff. apply lt_not_le. auto. }
-    rewrite H0. apply le_lt_weak in l. apply leb_true_iff in l. rewrite l. auto.
-  Qed.
-
-  Lemma ge_min_l: forall x y : Nt, min x y <= x.
-  Proof. 
-    intros.
-    unfold min. 
-    destruct (total_order_T x y).
-    {
-      destruct s.
-      2:{  rewrite e. destruct (leb y y); auto. }
-      apply le_lt_weak in l.
-      apply leb_true_iff in l. rewrite l. auto.
-    }
-    apply le_lt_weak.
-    apply le_lt_trans with y; auto.
-    apply lt_not_le in l. apply leb_false_iff in l.
-    rewrite l. auto.
-  Qed.
-
-  Lemma ge_min_r: forall x y : Nt, min x y <= y.
-  Proof. intros. rewrite min_comm. apply ge_min_l. Qed.
-
-  Lemma min_id: forall x : Nt, min x x = x.
-  Proof. intros. unfold min. destruct (leb x x); auto. Qed.
-
-  Lemma min_cases: forall x y : Nt, min x y = x \/ min x y = y.
-  Proof. intros. unfold min. destruct (leb x y); auto. Qed.
-
+ 
   End use_Numeric.
-
-
-
+(* 
+Instance Numeric_nat: Numerics.Numeric nat :=
+  @Numerics.mkNumeric
+    nat
+    Nat.add
+    (fun _ => O)
+    Nat.mul
+    Nat.pow
+    INR
+    id
+    O
+    (S O)
+    Nat.lt
+    le_gt_dec
+    Nat.eq_dec.
+ *)
 
 (**Req_EM_T**)
 Program Instance Numeric_D: Numerics.Numeric (DRed.t) :=
@@ -1620,14 +1645,26 @@ Program Instance Numeric_D: Numerics.Numeric (DRed.t) :=
     DRed.opp
     DRed.mult
     DRed.natPow
-    (fun x => Q2R (D_to_Q x))
     DRed.of_nat
     DRed.t0
     DRed.t1
     Dlt
-    DRed.lt_le_dec
-    DRed.eq_dec
+    Dlt_bool
+    DRed.eq_bool
 .
+Program Instance Numeric_DO: Numerics.Numeric (DORed.t) :=
+  @Numerics.mkNumeric
+    DORed.t
+    DORed.add
+    DORed.opp
+    DORed.mult
+    DORed.natPow
+    DORed.of_nat
+    DORed.t0
+    DORed.t1
+    DOlt
+    DOlt_bool
+    DORed.eq_bool.
 
 Program Instance Numeric_Props_D: @Numerics.Numeric_Props DRed.t Numeric_D:=
     @Numerics.mkNumericProps
@@ -1636,9 +1673,7 @@ Program Instance Numeric_Props_D: @Numerics.Numeric_Props DRed.t Numeric_D:=
     DRed.lt_t0_t1
     DRed.mult0L
     DRed.of_natO
-    DRed.of_nat_succ_l
-
-    
+    DRed.of_nat_succ_l    
     DRed.addC
     DRed.addA
     _
@@ -1653,17 +1688,69 @@ Program Instance Numeric_Props_D: @Numerics.Numeric_Props DRed.t Numeric_D:=
     DRed.mult_lt_compat_l
     DRed.natPowO
     DRed.natPowRec
-    _
-    _
-    _
-    _
-    _
     DRed.total_order_T
     _
-    _
-.
+    _.
 Next Obligation.
   intros. rewrite DRed.addC. apply DRed.addOppL. Qed.
+Next Obligation.
+  rewrite <- DRed.eq_bool_iff.
+  split; auto.
+Qed.
+Next Obligation.
+  rewrite <- Dlt_bool_iff.
+  split; auto.
+Qed.
+
+Program Instance Numeric_Props_DO: @Numerics.Numeric_Props DORed.t Numeric_DO:=
+    @Numerics.mkNumericProps
+    DORed.t
+    Numeric_DO
+    DORed.lt_t0_t1
+    DORed.mult0L
+    DORed.of_natO
+    DORed.of_nat_succ_l
+    DORed.addC
+    DORed.addA
+    _
+    DORed.add0l
+    DORed.multC
+    DORed.multA
+    DORed.mult1L
+    DORed.multDistrL
+    DORed.lt_asym
+    DORed.lt_trans
+    DORed.plus_lt_compat_l
+    DORed.mult_lt_compat_l
+    DORed.natPowO
+    DORed.natPowRec
+    DORed.total_order_T
+    _
+    _.
+Next Obligation.
+  intros. rewrite DORed.addC. apply DORed.addOppL. Qed.
+Next Obligation.
+  rewrite <- DORed.eq_bool_iff. split; auto.
+Qed.
+Next Obligation. 
+  rewrite <- DOlt_bool_iff. split; auto.
+Qed.
+
+Program Instance Numeric_R_Inj_DO: @Numerics.Numeric_R_inj DORed.t Numeric_DO:=
+  @mkNumericRInj _ _ (fun x => Q2R (DO_to_Q x)) _ _ _ _ _.
+Next Obligation.
+  intros;rewrite <- Q2R_plus;apply Qeq_eqR; rewrite DORed.addP; apply Qeq_refl. Qed.
+Next Obligation.
+  intros; rewrite <- Q2R_mult; apply Qeq_eqR; rewrite DORed.multP; apply Qeq_refl. Qed.
+Next Obligation.
+  intros. split;intros. apply Qlt_Rlt. auto. apply Rlt_Qlt. auto. Qed.
+Next Obligation.
+  intros. rewrite <- Q2R_opp. apply Qeq_eqR. rewrite DORed.oppP. apply Qeq_refl. Qed.
+Next Obligation.
+  intros. apply eqR_Qeq in H. apply DORed.DOred_eq; auto. Qed.
+
+Program Instance Numeric_R_Inj_D: @Numerics.Numeric_R_inj DRed.t Numeric_D :=
+  @mkNumericRInj _ _ (fun x => Q2R (D_to_Q x)) _ _ _ _ _.
 Next Obligation.
   intros;rewrite <- Q2R_plus;apply Qeq_eqR; rewrite DRed.addP; apply Qeq_refl. Qed.
 Next Obligation.
@@ -1674,31 +1761,6 @@ Next Obligation.
   intros. rewrite <- Q2R_opp. apply Qeq_eqR. rewrite DRed.oppP. apply Qeq_refl. Qed.
 Next Obligation.
   intros. apply eqR_Qeq in H. apply DRed.Dred_eq; auto. Qed.
-Next Obligation.
-  split; intros.
-  { 
-    destruct (DRed.eq_dec n m); auto.
-    by exfalso.
-  }
-  rewrite H.
-  destruct (DRed.eq_dec m m); auto.
-Qed.
-Next Obligation.
-  split; intros.
-  {
-    destruct (DRed.lt_le_dec n m); auto.
-    by exfalso.
-  }
-  destruct (DRed.lt_le_dec n m); auto.
-  exfalso.
-  by apply DRed.le_not_lt in H.
-Qed.
-
-
-
-Delimit Scope R_scope with R_s.
-Local Open Scope R_scope.
-
 
 Program Instance Numeric_R: Numeric R :=
   @Numerics.mkNumeric
@@ -1707,7 +1769,6 @@ Program Instance Numeric_R: Numeric R :=
     Ropp
     Rmult
     pow
-    (fun x => x)
     INR
     (IZR Z0)
     (IZR (Zpos xH))
@@ -1752,22 +1813,11 @@ Program Instance Numeric_Props_R: @Numerics.Numeric_Props R Numeric_R:=
     _
     _
     _
-
-    _
-    _
-    _
-    _
-    _
     Raxioms.total_order_T
     _
-    _
-.
+    _.
 Next Obligation. lra. Qed.
-Next Obligation.
-  rewrite -> Rplus_comm with 1 _.
-  destruct n; auto.
-  simpl. rewrite Rplus_0_l. auto.
-Qed.
+Next Obligation. induction n; simpl; lra. Qed.
 Next Obligation. lra. Qed.
 Next Obligation. lra. Qed. 
 Next Obligation. 
@@ -1783,7 +1833,6 @@ Next Obligation.
   repeat rewrite -> Rmult_comm with _ r.
   auto.
 Qed.
-Next Obligation. lra. Qed.
 Next Obligation. 
   unfold Numeric_R_obligation_2.
   destruct (Raxioms.total_order_T n m).
@@ -1822,6 +1871,10 @@ Next Obligation.
   by left.
 Qed.
 
+Program Instance Numeric_R_Inj_R: @Numerics.Numeric_R_inj R Numeric_R:=
+  @mkNumericRInj _ _ id _ _ _ _ _.
+Next Obligation. lra. Qed.
+
 Lemma to_R_R: forall x : R, to_R x = x.
 Proof. intros. simpl. auto. Qed.
 
@@ -1839,11 +1892,9 @@ Program Instance Numeric_z : Numerics.Numeric Z :=
     Z.opp
     Z.mul
     Zpower_nat
-    IZR
     Z.of_nat
     Z0
     (Zpos (1)%positive)
-
     Z.lt
     Z.ltb
     Z.eqb.
@@ -1871,17 +1922,10 @@ Program Instance Numeric_Props_z : @Numerics.Numeric_Props Z Numeric_z :=
     _
     _
     _
-    _
-
     _
     _
     _
-    _
-    eq_IZR
-    _
-    Z.eqb_eq
-    Z.ltb_lt
-.
+    _.
 Next Obligation. lia. Qed.
 Next Obligation. 
   fold (Z.of_nat n.+1).
@@ -1899,6 +1943,19 @@ Next Obligation.
   repeat rewrite -> Zmult_comm with _ r.
   auto.
 Qed.
+Next Obligation.
+  destruct Z_dec' with r1 r2; auto.
+  destruct s; auto.
+Qed.
+Next Obligation. 
+  split; intros; apply Z.eqb_eq; auto.
+Qed.
+Next Obligation.
+  split; intros; apply Z.ltb_lt; auto.
+Qed.
+
+Program Instance Numeric_R_Inj_z: @Numerics.Numeric_R_inj Z Numeric_z :=
+  @mkNumericRInj _ _ IZR _ _ _ _ _.
 Next Obligation. rewrite plus_IZR. auto. Qed.
 Next Obligation. rewrite mult_IZR. auto. Qed. 
 Next Obligation. 
@@ -1907,13 +1964,7 @@ Next Obligation.
   apply lt_IZR.
 Qed.
 Next Obligation. rewrite opp_IZR. auto. Qed.
-Next Obligation.
-  destruct Z_dec' with r1 r2; auto.
-  destruct s; auto.
-Qed.
-    
-    
- 
+Next Obligation. apply eq_IZR. auto. Qed.
 
   Delimit Scope R_scope with R_s.
 
@@ -1928,7 +1979,7 @@ Qed.
   Local Open Scope Numeric_scope.
 
   Section use_Numeric2.
-  Context {Nt:Type} {H : Numeric Nt} `{NtProps : Numeric_Props (numeric_t := H) Nt}.
+  Context {Nt:Type} {H : Numeric Nt} `{NtProps : Numeric_Props (numeric_t := H) Nt} {Nt_R_inj : @Numeric_R_inj Nt H}.
 
   Lemma to_R_eqb: forall (n m : Nt), eqb n m = eqb (to_R n) (to_R m).
   Proof.
@@ -2018,6 +2069,8 @@ Qed.
 
 End use_Numeric2.
 
+
+
 Definition log (x y : R) := Rdiv (ln y) (ln x).
     
 Lemma ln_pow: forall (x : R) (n : nat), 0 < x -> ln (x ^ n) = INR n * ln x.
@@ -2253,13 +2306,13 @@ Qed.
 
 
   Section use_Numeric3.
-  Context {Nt : Type } `{Numeric_Props Nt}.
+  Context {Nt : Type } `{Numeric_Props Nt} `{Nt_to_R : @Numeric_R_inj Nt numeric_t }.
 
   Lemma exists_pow_nat_le: forall x y : Nt, 0 < x -> x < 1 -> 0 < y -> exists n, Numerics.pow_nat x n <= y.
   Proof.
     intros.
     destruct exists_pow_le with (to_R x) (to_R y); auto.
-    { simpl; rewrite <- to_R_plus_id; apply to_R_lt; auto. }
+    { simpl; rewrite <- to_R_plus_id; rewrite <- to_R_lt; auto. }
     { simpl; rewrite <- to_R_mult_id; apply to_R_lt; auto. }
     { simpl; rewrite <- to_R_plus_id; apply to_R_lt; auto. }
     exists x0.