diff --git a/doc/part-hydras.tex b/doc/part-hydras.tex
index 0b7dea2b..5fbd436a 100644
--- a/doc/part-hydras.tex
+++ b/doc/part-hydras.tex
@@ -1701,24 +1701,25 @@ \section{Ordinal Notations}
 
 
 
-\subsection{A class for ordinal notations}
+\subsection{Classes for ordinal notations}
 
 From the \coq{} user's point of view, an ordinal notation is
 a structure allowing to compare two ordinals by computation, and proving by well-founded induction.
 
-\subsubsection{The \texttt{Comparable class}}
+\subsubsection{The \texttt{Comparison} and \texttt{Comparable} classes}
 
-The following class, contributed by Jérémy Damour and Théo Zimmermann, allows us to apply generic lemmas and tactics
-about decidable strict orders.
+We use the operational class \texttt{Comparison} of comparison functions to define the \texttt{Comparable} class, contributed by Jérémy Damour and Théo Zimmermann, which allows us to apply generic lemmas and tactics about decidable strict orders.
 The correctness of the comparison function is expressed through Stdlib's type 
-\texttt{Datatypes.CompareSpec}.
-
+\texttt{Datatypes.CompareSpec} as specialized by \texttt{Datatypes.CompSpec}.
 
 \begin{Coqsrc}
 Inductive CompareSpec (Peq Plt Pgt : Prop) : comparison -> Prop :=
     CompEq : Peq -> CompareSpec Peq Plt Pgt Eq
   | CompLt : Plt -> CompareSpec Peq Plt Pgt Lt
   | CompGt : Pgt -> CompareSpec Peq Plt Pgt Gt.
+
+Definition CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop :=
+ CompareSpec (eq x y) (lt x y) (lt y x).
 \end{Coqsrc}
 
 \emph{From Module~\href{../theories/html/hydras.Prelude/mparable.html\#Hvariant}{Prelude.Comparable}}
diff --git a/theories/gaia/T1Bridge.v b/theories/gaia/T1Bridge.v
index 1e4d2837..9e565048 100644
--- a/theories/gaia/T1Bridge.v
+++ b/theories/gaia/T1Bridge.v
@@ -1,9 +1,7 @@
 (**  * Bridge between Hydra-battle's and Gaia's [T1]  (Experimental) 
  *)
 
-
-
-
+From hydras Require Import DecPreOrder.
 From hydras Require T1.
 From mathcomp Require Import all_ssreflect zify.
 From gaia Require Import ssete9.
@@ -109,18 +107,18 @@ Proof.
 Qed.
 
 Lemma compare_ref x :
-  forall y, match T1.compare x y with
+  forall y, match T1.compare_T1 x y with
   | Lt => T1lt (iota x) (iota y)
   | Eq => iota x = iota y
   | Gt => T1lt (iota y) (iota x)
   end.
 Proof.
 elim: x => [|x1 IHx1 n x2 IHx2]; case => //= y1 n0 y2.
-case H: (T1.compare x1 y1).
+case H: (T1.compare_T1 x1 y1).
 - specialize (IHx1 y1); rewrite H in IHx1.
   case H0: (PeanoNat.Nat.compare n n0).
   + have ->: (n = n0) by apply Compare_dec.nat_compare_eq.
-    case H1: (T1.compare x2 y2).
+    case H1: (T1.compare_T1 x2 y2).
     * rewrite IHx1; f_equal.
       by specialize (IHx2 y2); now rewrite H1 in IHx2.
     * case (iota x1 < iota y1); [trivial|].
@@ -141,9 +139,10 @@ Qed.
 Lemma lt_ref (a b : hT1): T1.lt a b <-> (iota a < iota b).
 Proof.
   split.
-  - rewrite /T1.lt; move => Hab; generalize (compare_ref a b); now rewrite Hab.
+  - rewrite /T1.lt /Comparable.compare; move => Hab. 
+    generalize (compare_ref a b); now rewrite Hab.
   - move => Hab; red.
-    case_eq (T1.compare a b).
+    case_eq (T1.compare_T1 a b).
     + move => Heq; generalize (compare_ref a b); rewrite Heq.
       move => H0; move: Hab; rewrite H0;
                 move => Hb; by rewrite T1ltnn in Hb.
@@ -166,11 +165,12 @@ Qed.
 Lemma plus_ref : refines2 T1.plus T1add.
 Proof.
   move => x; elim: x => [|x1 IHx1 n x2 IHx2]; case => //= y1 n0 y2.
-  case Hx1y1: (T1.compare x1 y1); move: (compare_ref x1 y1); rewrite Hx1y1 => H.
-  - by rewrite H T1ltnn /=; f_equal.
-  - by rewrite H /=; f_equal.
+  case Hx1y1: (T1.compare_T1 x1 y1); move: (compare_ref x1 y1); rewrite Hx1y1 => H.
+  - rewrite /Comparable.compare H T1ltnn /=; f_equal.
+    by rewrite Hx1y1 -H /=.
+  - by rewrite /Comparable.compare H Hx1y1.
   - replace (iota x1 < iota y1) with false.
-    rewrite H /=; f_equal.
+    rewrite /Comparable.compare H /= Hx1y1; f_equal.
     change (cons (iota y1) n0 (iota y2)) with (iota (T1.ocons y1 n0 y2)).
       by rewrite IHx2.
         by apply T1lt_anti in H.
@@ -284,28 +284,32 @@ Proof.
   by rewrite -(pi_iota a) -(pi_iota b) -(pi_iota c) !mult_refR mulA. 
 Qed.
 
-
-Lemma Comparable_T1lt_eq  a b:
-  Comparable.lt_b a b = (iota a < iota b).
+Lemma Comparable_T1lt_eq a b:
+  bool_decide (T1.lt a b) = (iota a < iota b).
 Proof.
-  rewrite /Comparable.lt_b; generalize (compare_ref a b). 
-  case_eq (T1.compare a b).    
-  - move => _ ->;  by rewrite T1ltnn.
-  - by []. 
-  - move => _ H; case_eq (iota a < iota b). 
-    + move => H0; have H1 : (iota b < iota b)  by
-                  apply T1lt_trans with (iota a).
-        by rewrite T1ltnn in H1. 
-    + by [].
+  rewrite /T1.lt; generalize (compare_ref a b);
+  rewrite /Comparable.compare /=.
+  destruct (decide (T1.compare_T1 a b = Lt)).
+  - have bd := e.
+    apply (bool_decide_eq_true _) in bd.
+    by rewrite bd e.
+  - have bd := n.
+    apply (bool_decide_eq_false _) in bd.
+    rewrite bd.
+    destruct (T1.compare_T1 a b).
+    * by move => ->; rewrite T1ltnn.
+    * by [].
+    * move => Hlt.
+      symmetry.
+      apply/negP => Hlt'.
+      have H1 : (iota b < iota b) by apply T1lt_trans with (iota a).
+      by rewrite T1ltnn in H1.
 Qed.
 
-
 Lemma nf_ref a : T1.nf_b a = T1nf (iota a).
 Proof.
   elim: a => //.
   - move => a IHa n b IHb; rewrite T1.nf_b_cons_eq; simpl T1nf. 
     rewrite IHa IHb;  change (phi0 (iota a)) with (iota (T1.phi0 a)).
-    rewrite andbA; cbn; by rewrite Comparable_T1lt_eq.
+    by rewrite andbA Comparable_T1lt_eq.
 Qed.
-
- 
diff --git a/theories/ordinals/Epsilon0/Canon.v b/theories/ordinals/Epsilon0/Canon.v
index 8749c158..ae617a15 100644
--- a/theories/ordinals/Epsilon0/Canon.v
+++ b/theories/ordinals/Epsilon0/Canon.v
@@ -13,6 +13,7 @@ Pierre Casteran,
 From Coq Require Export Arith Lia.
 Import Relations Relation_Operators.
 
+From hydras.Prelude Require Import DecPreOrder.
 From hydras.Epsilon0 Require Export T1 E0.
 
 Set Implicit Arguments.
@@ -916,7 +917,7 @@ Fixpoint  approx alpha beta fuel i :=
           FO => None
         | Fuel.FS f =>
           let gamma := canonS alpha i in
-          if lt_b beta gamma
+          if decide (lt beta gamma)
           then Some (i,gamma)
           else approx alpha beta  (f tt) (S i)
         end.
@@ -924,12 +925,12 @@ Fixpoint  approx alpha beta fuel i :=
 
 Lemma approx_ok alpha beta :
   forall fuel i j gamma, approx alpha beta fuel i = Some (j,gamma) ->
-                         gamma = canonS alpha j /\ lt_b beta gamma.
+                         gamma = canonS alpha j /\ lt beta gamma.
 Proof.
   induction fuel as [| f IHfuel ].
   - cbn; discriminate. 
   - intros i j gamma H0;  cbn in H0.
-    case_eq (lt_b beta (canonS alpha i));intro H1; rewrite H1 in *.
+    destruct (decide (lt beta (canonS alpha i))) as [H1|H1].
     + injection H0; intros; subst; split;auto.
     + now specialize (IHfuel tt (S i) _ _ H0).
 Qed.
diff --git a/theories/ordinals/Epsilon0/E0.v b/theories/ordinals/Epsilon0/E0.v
index 32ee80a2..85455853 100644
--- a/theories/ordinals/Epsilon0/E0.v
+++ b/theories/ordinals/Epsilon0/E0.v
@@ -316,12 +316,11 @@ Proof.
     apply LT_trans.
  Qed.
 
-Definition compare (alpha beta:E0): comparison :=
-  T1.compare (cnf alpha) (cnf beta).
+Instance compare_E0 : Compare E0 :=
+ fun (alpha beta:E0) => compare (cnf alpha) (cnf beta).
 
-Lemma compare_correct alpha beta :
-  CompareSpec (alpha = beta) (alpha o< beta) (beta o< alpha)
-              (compare alpha beta).
+Lemma compare_correct (alpha beta : E0) :
+  CompSpec eq Lt alpha beta (compare alpha beta).
 Proof.
   destruct alpha, beta; unfold compare, Lt; cbn;
     destruct (T1.compare_correct cnf0 cnf1).
diff --git a/theories/ordinals/Epsilon0/Hessenberg.v b/theories/ordinals/Epsilon0/Hessenberg.v
index b0900262..54953087 100644
--- a/theories/ordinals/Epsilon0/Hessenberg.v
+++ b/theories/ordinals/Epsilon0/Hessenberg.v
@@ -359,8 +359,9 @@ Proof.
   - intros; rewrite (oplus_eqn  (ocons a n b) (ocons x1 n0 x2)).
     apply nf_helper_phi0 in H1.
     destruct (lt_inv H1).
-    + unfold T1.lt, lt_b in H2; rewrite compare_rev. 
-      destruct (compare x1 a);auto; try discriminate. 
+    + unfold T1.lt in H2.
+      rewrite compare_rev, H2.
+      reflexivity.
     + decompose [or and] H2.
       *  inversion H5.
       * T1_inversion H6.
@@ -522,7 +523,7 @@ Section Proof_of_oplus_lt1.
     -  simpl; auto with T1.
     - rewrite oplus_eqn;case_eq (compare x1 a1).
       +  auto with T1 arith. 
-      +  intros H2; apply head_lt; unfold T1.lt, lt_b; now  rewrite H2. 
+      +  intros H2; apply head_lt. unfold T1.lt; now  rewrite H2. 
       + intro; apply tail_lt,  H1 ;  trivial.
         eapply nf_inv2, H.
         now  apply tail_lt_ocons.
@@ -619,7 +620,7 @@ Proof with eauto with T1.
        absurd  (T1.lt (ocons a1 n0 b2) (ocons c1 n1 c2)).
        - apply lt_not_gt.
          apply head_lt.
-         unfold T1.lt, lt_b;rewrite compare_rev. now   rewrite H2.
+         unfold T1.lt;rewrite compare_rev. now   rewrite H2.
        -   auto.
      }
      {
@@ -652,7 +653,7 @@ Proof with eauto with T1.
            case_eq (compare a1 c2_1).
            intro.
            apply coeff_lt;  auto with arith. 
-           intro H6; apply head_lt; unfold T1.lt, lt_b; now rewrite H6.
+           intro H6; apply head_lt; unfold T1.lt; now rewrite H6.
            intros; apply tail_lt. 
            apply oplus_lt1; trivial.
            T1_inversion H5.
diff --git a/theories/ordinals/Epsilon0/Paths.v b/theories/ordinals/Epsilon0/Paths.v
index db70594c..5474db4e 100644
--- a/theories/ordinals/Epsilon0/Paths.v
+++ b/theories/ordinals/Epsilon0/Paths.v
@@ -14,7 +14,7 @@
 
 (** TODO: Check wether the predicates ...PathS... are still useful *)
 
-Require Import Canon  MoreLists First_toggle OrdNotations.
+From hydras Require Import DecPreOrder Canon MoreLists First_toggle OrdNotations.
 Import Relations Relation_Operators.
 From Coq Require Import Lia.
 
@@ -2592,23 +2592,22 @@ Section Constant_to_standard_Proof.
     unfold t; pattern (proj1_sig Rem2); apply proj2_sig.
   Qed. 
 
-  Let P (i:nat) := le_b beta (standard_gnaw (S n) alpha i).
+  Let P (i:nat) := compare (standard_gnaw (S n) alpha i) beta <> Datatypes.Lt.
 
   Remark Rem04 : P 0.
   Proof.
-    unfold P;red; simpl.  
-    unfold le_b, lt_b.
-    eenough (T1.compare alpha beta = Datatypes.Gt) as -> by auto.
+    unfold P;red; simpl.
+    enough (Hgt: (compare alpha beta = Datatypes.Gt)) by congruence.
     apply compare_gt_iff.
     generalize (const_pathS_LT Halpha Hpa).
     destruct 1; tauto.
-  Qed. 
+  Qed.
 
 
-  Remark Rem05 : P t = false.
+  Remark Rem05 : ~ P t.
   Proof.
-    unfold P, le_b, lt_b;
-    enough(T1.compare (standard_gnaw (S n) alpha t) beta = Datatypes.Lt) as -> by reflexivity.
+    unfold P.
+    enough (compare (standard_gnaw (S n) alpha t) beta = Datatypes.Lt) by congruence.
     apply compare_lt_iff.
     destruct Rem03; tauto.
   Qed.
@@ -2621,8 +2620,21 @@ Section Constant_to_standard_Proof.
        eapply const_pathS_LT; eauto.
     - auto with arith. 
   Qed.
+
+  Instance P_dec i : Decision (P i).
+  Proof.
+   destruct (compare (standard_gnaw (S n) alpha i) beta) eqn:Hc.
+   - left; unfold P.
+     rewrite Hc; discriminate.
+   - right; unfold P.
+     rewrite Hc.
+     intro H.
+     contradiction.
+   - left; unfold P.
+     rewrite Hc; discriminate.
+  Defined.
   
-  Let l_def :=  first_toggle P 0 t  Rem06 Rem04 Rem05.
+  Let l_def :=  first_toggle P P_dec 0 t  Rem06 Rem04 Rem05.
 
   Let l := proj1_sig l_def.
   
@@ -2633,7 +2645,7 @@ Section Constant_to_standard_Proof.
     (l < t)%nat /\
     (forall i : nat,
         (0 <= i)%nat ->
-        (i <= l)%nat -> P i = true) /\ P (S l) = false.
+        (i <= l)%nat -> P i) /\ ~ P (S l).
   Proof.
     unfold l; pattern (proj1_sig l_def); apply proj2_sig.
   Qed.
@@ -2641,13 +2653,13 @@ Section Constant_to_standard_Proof.
   Remark Rem09 : (l < t)%nat.
   Proof.   destruct Rem08; tauto. Qed.
 
-  Remark Rem10 : P l = true.
+  Remark Rem10 : P l.
   Proof.
     destruct Rem08 as [H H0];decompose [and] H0.
     apply H3; auto with arith.
   Qed.
   
-  Remark Rem11 : P (S l) = false.
+  Remark Rem11 : ~ P (S l).
   Proof.
     destruct Rem08 as [H H0]; now decompose [and] H0.  
   Qed.
@@ -2726,13 +2738,13 @@ Section Constant_to_standard_Proof.
 
   Remark R19 : beta t1<= gamma.
   Proof.
-    generalize Rem10; unfold P; fold gamma ;unfold le_b, lt_b.
+    generalize Rem10; unfold P; fold gamma.
     intro H.
-    destruct (T1.compare gamma beta) eqn: Hcomp.
+    destruct (compare gamma beta) eqn: Hcomp.
     - apply compare_eq_iff in Hcomp as ->.
       apply LE_refl.
       eapply LT_nf_r; eauto.
-    - intros; discriminate.
+    - contradiction.
     - apply LE_r.
       rewrite compare_gt_iff in Hcomp; repeat split; auto.
       + eapply LT_nf_r; eauto.
@@ -2787,15 +2799,14 @@ Section Constant_to_standard_Proof.
 
    Remark R25 : delta t1< beta.
   Proof.
-    rewrite R22; generalize Rem11;unfold P; intro H;
-      unfold le_b, lt_b in H.
-    destruct( T1.compare (standard_gnaw (S n) alpha (S l)) beta) eqn: H0.
-    - discriminate.
+    rewrite R22; generalize Rem11;unfold P; intro H.      
+    destruct(compare (standard_gnaw (S n) alpha (S l)) beta) eqn: H0.
+    - contradict H; congruence.
     - rewrite compare_lt_iff in H0.
        repeat split;auto.
        +  apply standard_gnaw_nf;auto.
        +  eapply LT_nf_r; eauto.
-    - discriminate.
+    - contradict H; congruence.
   Qed.
 
    Remark R26 : ~ const_pathS (n+l) gamma beta.
@@ -3021,7 +3032,7 @@ Proof.
      red in H0;unfold E0.cnf; simpl in *.
      destruct beta.
      + destruct H; now apply E0_eq_intro.
-     + destruct (T1.compare alpha beta1) eqn:H2.
+     + destruct (compare alpha beta1) eqn:H2.
          * unfold lt in H1; simpl in H1.
            rewrite compare_eq_iff in H2;  subst beta1.
            destruct (LT_inv H1).
diff --git a/theories/ordinals/Epsilon0/T1.v b/theories/ordinals/Epsilon0/T1.v
index 73e49499..e6e91b1b 100644
--- a/theories/ordinals/Epsilon0/T1.v
+++ b/theories/ordinals/Epsilon0/T1.v
@@ -146,24 +146,24 @@ Inductive ap : T1 -> Prop :=
  *)
 
 (* begin snippet compareDef *)
-
-Fixpoint compare (alpha beta:T1):comparison :=
+Instance compare_T1 : Compare T1 :=
+ fix cmp (alpha beta:T1) :=
   match alpha, beta with
   | zero, zero => Eq
   | zero, ocons a' n' b' => Lt
   | _   , zero => Gt
   | (ocons a n b),(ocons a' n' b') =>
-      (match compare a a' with 
+      (match cmp a a' with
        | Lt => Lt
        | Gt => Gt
-       | Eq => (match Nat.compare n n' with
-                | Eq => compare b b'
+       | Eq => (match n ?= n' with
+                | Eq => cmp b b'
                 | comp => comp
                 end)
        end)
   end.
 
-Definition lt alpha beta : Prop :=
+Definition lt (alpha beta : T1) : Prop :=
   compare alpha beta = Lt.
 (* end snippet compareDef *)
 
@@ -177,24 +177,38 @@ Proof. discriminate.  Qed.
 
 (** ** Properties of [compare] *)
 
+Lemma compare_ocons : 
+ forall a n b a' n' b',
+ compare (ocons a n b) (ocons a' n' b') =
+ match compare a a' with
+ | Lt => Lt
+ | Gt => Gt
+ | Eq => (match n ?= n' with
+        | Eq => compare b b'
+        | comp => comp
+        end)
+ end.
+Proof.
+intros; reflexivity.
+Qed.
+
 (* begin snippet compareRev *)
 
 Lemma compare_rev :
-  forall alpha beta,
+  forall (alpha beta : T1),
   compare beta alpha = CompOpp (compare alpha beta). (* .no-out *)
 Proof. (* .no-out *)
   induction alpha, beta. (* .unfold -.g#* .g#1 *)
   (* end snippet compareRev *)
-  
+
   1-3: easy.
-  simpl.
+  rewrite !compare_ocons.
   rewrite IHalpha1, Nat.compare_antisym.
-  destruct (compare alpha1 beta1).
+  destruct (compare alpha1 beta1); simpl.
   2-3: easy.
   now destruct (n ?= n0) eqn:?; simpl.
 Qed.
 
-
 Lemma compare_reflect :
   forall alpha beta,
     match compare alpha beta with
@@ -205,9 +219,9 @@ Lemma compare_reflect :
 Proof.
   unfold lt; induction alpha, beta.
   1-3: easy.
-  simpl.
   specialize (IHalpha1 beta1).
   specialize (IHalpha2 beta2).
+  rewrite !compare_ocons.
   rewrite compare_rev with alpha1 beta1,
           compare_rev with alpha2 beta2,
           Nat.compare_antisym in *.
@@ -220,8 +234,7 @@ Proof.
 Qed.
 
 Lemma compare_correct (alpha beta: T1):
-  CompareSpec (alpha = beta) (lt alpha beta) (lt beta alpha)
-              (compare alpha beta).
+  CompSpec eq lt alpha beta (compare alpha beta).
 Proof.
   unfold lt.
   generalize (compare_reflect alpha beta).
@@ -231,14 +244,14 @@ Qed.
 (** ** Properties of Eq *)
 
 Lemma compare_refl :
-  forall alpha, compare alpha alpha = Eq.
+  forall alpha : T1, compare alpha alpha = Eq.
 Proof.
  induction alpha; cbn; auto.
  rewrite IHalpha1, IHalpha2.
  now rewrite Nat.compare_refl.
 Qed.
 
-Lemma compare_eq_iff a b : 
+Lemma compare_eq_iff (a b : T1) : 
   compare a b = Eq <-> a = b.
 Proof.
   split; intro H.
@@ -283,7 +296,7 @@ Lemma lt_inv_strong :
   lt_cases a b n a' b' n'.
 Proof.
   unfold lt.
-  intros; simpl in H.
+  intros; rewrite compare_ocons in H.
   destruct (compare a a') eqn:Ha.
   - apply compare_eq_iff in Ha as ->.
     destruct (n ?= n') eqn:?.
@@ -371,7 +384,7 @@ Lemma head_lt :
 Proof.
   unfold lt.
   intros * H.
-  simpl.
+  rewrite compare_ocons.
   now rewrite H.
 Qed.
 
@@ -381,7 +394,7 @@ Lemma coeff_lt :
 Proof.
   unfold lt.
   intros * H.
-  simpl.
+  rewrite compare_ocons.
   rewrite compare_refl.
   now apply Nat.compare_lt_iff in H as ->.
 Qed.
@@ -395,7 +408,7 @@ Lemma tail_lt :
 Proof.
   unfold lt.
   intros * H.
-  simpl.
+  rewrite compare_ocons.
   now rewrite compare_refl, Nat.compare_refl.
 Qed.
 
@@ -407,8 +420,8 @@ Lemma compare_fin_rw (n n1: nat) :
   - easy.
   - now cbn.
   - now cbn.
-  - cbn; case (n ?= n1); trivial.
-Qed. 
+  - cbn; unfold compare; case (n ?= n1); trivial.
+Qed.
 
 Lemma lt_fin_iff (i j : nat): lt (fin i) (fin j) <-> Nat.lt i j.
 Proof.
@@ -417,9 +430,11 @@ Proof.
   - split; [ auto with arith| cbn; constructor ].
   - split; inversion 1.
   - split; inversion 1.
-     + destruct (Nat.compare_spec i j); try discriminate.
-        auto with arith. 
-     +   apply coeff_lt; auto with arith.   
+     + unfold compare in H1.
+       simpl in H1.
+       destruct (Nat.compare_spec i j); try discriminate.
+       auto with arith. 
+     + apply coeff_lt; auto with arith.
      + apply coeff_lt; lia.
 Qed.
 
@@ -490,6 +505,9 @@ Qed.
 Cantor normal form needs the exponents of omega to be
    in strict decreasing order *)
 
+Instance lt_dec : RelDecision lt :=
+fun alpha beta => decide (compare alpha beta = Lt).
+
 (* begin snippet nfDef *)
 
 Fixpoint nf_b (alpha : T1) : bool :=
@@ -497,7 +515,7 @@ Fixpoint nf_b (alpha : T1) : bool :=
   | zero => true
   | ocons a n zero => nf_b a
   | ocons a n ((ocons a' n' b') as b) =>
-      (nf_b a && nf_b b && lt_b a' a)%bool
+      (nf_b a && nf_b b && (bool_decide (lt a' a)))%bool
   end.
 
 Definition nf alpha :Prop := 
@@ -671,7 +689,7 @@ Proof.
   unfold nf.
   simpl.
   intros a n a' n' b' Hlta Ha.
-  apply lt_b_iff in Hlta as ->.
+  apply (bool_decide_eq_true _) in Hlta.
   destruct b'.
   - intro Hnfa'.
     now rewrite Ha, Hnfa'.
@@ -708,7 +726,7 @@ Proof.
   unfold nf; cbn;
   destruct a, a', b'; try discriminate; auto with T1;
   intro H; red in H; repeat rewrite andb_true_iff in H; 
-  decompose [and] H; apply lt_b_iff; auto.
+  decompose [and] H; apply (bool_decide_eq_true _); auto.
 Qed.
 
 
@@ -719,7 +737,8 @@ Proof.
   -  repeat split; auto with T1.
   - intro H; red in H; repeat rewrite andb_true_iff in H;
    decompose [and]  H; repeat split; auto.
-   red; cbn; unfold lt_b in H1; destruct (compare b1 a); try discriminate. 
+   apply bool_decide_eq_true in H1; red in H1.
+   red; cbn; destruct (compare b1 a); try discriminate. 
    trivial. 
 Qed. 
 
@@ -747,26 +766,24 @@ Proof.
     assert (false)  by (now apply H0);  discriminate.
 Qed.
 
-
-Lemma lt_b_lt_iff a b : lt_b a b <-> lt a b.
-Proof.
-  split.
-  - intro H;red in H; now rewrite lt_b_iff in H.  
-  - intro; red; now rewrite  lt_b_iff.
-Qed.
-
-
 Lemma nf_b_cons_eq a n b : nf_b (ocons a n b) =
-                           nf_b a && nf_b b && lt_b b (phi0 a).
+                           nf_b a && nf_b b && bool_decide (lt b (phi0 a)).
 Proof.
   rewrite bool_eq_iff; generalize (nf_cons_iff a n b); unfold nf;
     intro H; rewrite H.
-  rewrite <- lt_b_lt_iff; split. 
-  -  case (nf_b a); case (nf_b b); case_eq (lt_b b (phi0 a));
-       cbn; auto with bool;
-         intros _ H0; decompose [and] H0; try discriminate.
-  -  intro H0;  red in H0; repeat rewrite andb_true_iff in H0; 
-       decompose [and] H0;  now rewrite H2, H3, H4.
+  destruct (decide (lt b (phi0 a))) as [Hdec|Hdec].
+  - pose proof Hdec as Heq.
+    rewrite <- (bool_decide_eq_true _) in Heq.
+    split; case (nf_b a); case (nf_b b);
+      cbn; auto with bool; intros H0;
+        decompose [and] H0; try discriminate.
+  - pose proof Hdec as Heq.
+    rewrite <- (bool_decide_eq_false _) in Heq.
+    rewrite Heq.
+    split; intro H0; repeat rewrite andb_true_iff in H0; 
+       decompose [and] H0; [congruence|].
+    rewrite andb_false_r in H0.
+    discriminate.
 Qed.
 
       
@@ -863,7 +880,7 @@ Proof.
   intros; simpl in H. unfold lt in H.
   destruct (compare _ _) eqn:?.
   1,3: easy.
-  simpl in *.
+  unfold compare in Heqc; simpl in Heqc.
   destruct (n ?= p) eqn:?.
   1,3: easy.
   now apply Nat.compare_lt_iff.
@@ -1141,7 +1158,7 @@ Proof.
   - red in H.
     repeat rewrite andb_true_iff in H. 
     destruct H as ((_, _), Hlt).
-    apply lt_b_iff in Hlt.
+    apply bool_decide_eq_true in Hlt.
     now right.
 Qed.
 
@@ -2035,6 +2052,7 @@ Proof.
     1-3: discriminate.
     simpl.
     intros * Hnf_1 Hnf_2.
+    rewrite compare_ocons.
     destruct (compare alpha0 alpha) eqn:?.
     2-3: easy.
     destruct (n2 ?= n1) eqn:?.
@@ -2707,7 +2725,7 @@ Proof.
     + assert (H0 :alpha2 = zero).
       { eapply nf_of_finite; eauto. }
       subst; rewrite plus_compat; f_equal;  ring.
-    + simpl; repeat rewrite compare_refl. rewrite Nat.compare_refl.
+    + simpl; repeat rewrite compare_refl. 
       f_equal; lia.
 Qed.
 
@@ -3882,26 +3900,33 @@ Section Proof_of_dist.
     destruct b1, a1; try destruct c1; simpl.
     5,7,9,11,13-16: now apply not_lt_zero in Hcomp_b1_c1.
     - f_equal; lia.
-    - rewrite Nat.compare_refl, !compare_refl.
+    - rewrite compare_ocons.
+      rewrite Nat.compare_refl, !compare_refl.
       f_equal; lia.
-    - now rewrite Nat.compare_refl, !compare_refl.
+    - rewrite compare_ocons.
+      now rewrite Nat.compare_refl, !compare_refl.
     - rewrite compare_refl.
       now destruct (compare a1_1 b1_1).
     - reflexivity.
     - compare destruct a1_1 c1_1 as Hcomp_a11_c11.
-      + rewrite compare_refl.
+      + rewrite compare_ocons.
+        rewrite compare_refl.
         enough (Nat.compare n2 (S (n2 + n3)) = Lt) as -> by reflexivity.
         apply Nat.compare_lt_iff; lia.
-
-      + now apply compare_lt_iff in Hcomp_a11_c11 as ->.
-      + rewrite compare_refl, Nat.compare_refl.
+      + rewrite compare_ocons.
+        now apply compare_lt_iff in Hcomp_a11_c11 as ->.
+      + rewrite compare_ocons.
+        rewrite compare_refl, Nat.compare_refl.
         eenough (compare a1_2 (a1_2 + _) = Lt) as -> by reflexivity.
         apply compare_lt_iff, lt_plus_l.
     - apply lt_inv_strong in Hcomp_b1_c1 as [Hlt | Heqa  Hlt | Heqa Heqn Hlt].
-      + now apply compare_lt_iff in Hlt as ->.
-      + rewrite Heqa, compare_refl.
+      + rewrite compare_ocons.
+        now apply compare_lt_iff in Hlt as ->.
+      + rewrite compare_ocons.
+        rewrite Heqa, compare_refl.
         now apply Nat.compare_lt_iff in Hlt as ->.
-      + rewrite Heqa, Heqn, compare_refl, Nat.compare_refl.
+      + rewrite compare_ocons.
+        rewrite Heqa, Heqn, compare_refl, Nat.compare_refl.
         now apply compare_lt_iff in Hlt as ->.
     - compare destruct a1_1 c1_1 as Hcomp_a11_c11.
       + apply lt_inv_strong in Hcomp_b1_c1 as [Hlt | Heqa  Hlt | Heqa Heqn Hlt].
@@ -3942,10 +3967,13 @@ Section Proof_of_dist.
     -  rewrite_ind Hind b2. 
     -  rewrite_ind Hind b2.
        apply lt_inv_strong in Hcomp_b1_c1 as [Hlt | Heqa  Hlt | Heqa Heqn Hlt].
-       + now apply compare_gt_iff in Hlt as ->. 
-       + rewrite Heqa, compare_refl.
+       + rewrite compare_ocons.
+         now apply compare_gt_iff in Hlt as ->. 
+       + rewrite compare_ocons.
+         rewrite Heqa, compare_refl.
          now apply Nat.compare_gt_iff in Hlt as ->.
-       + rewrite Heqa, Heqn, compare_refl, Nat.compare_refl.
+       + rewrite compare_ocons.
+         rewrite Heqa, Heqn, compare_refl, Nat.compare_refl.
          now apply compare_gt_iff in Hlt as ->.
     -  rewrite_ind Hind b2.
        compare destruct a1_1 b1_1 as Hcomp_a11_b11.
diff --git a/theories/ordinals/Gamma0/Gamma0.v b/theories/ordinals/Gamma0/Gamma0.v
index d5625615..e5f7bb97 100644
--- a/theories/ordinals/Gamma0/Gamma0.v
+++ b/theories/ordinals/Gamma0/Gamma0.v
@@ -298,7 +298,8 @@ Defined.
 
 (* begin snippet compare *)
 
-Definition compare (t1 t2 : T2) : comparison := 
+Instance compare_T2 : Compare T2 := 
+fun (t1 t2 : T2) =>
   match lt_eq_lt_dec t1 t2 with
   | inleft (left _) => Lt
   | inleft (right _) => Eq
@@ -787,7 +788,7 @@ Lemma compare_reflect alpha beta : match compare alpha beta with
                                      | Gt => beta t2< alpha
                                      end.
 Proof.
-  unfold compare.
+  unfold compare,compare_T2.
   intros; case (lt_eq_lt_dec alpha beta);auto.
   destruct s;auto with T2.
 Qed.
@@ -814,7 +815,7 @@ Qed.
 Example Ex6 : gcons 1 0 12 omega t2< [0,[2,1]].
 Proof. now apply compare_Lt. Qed.
 
-Lemma compare_Eq : forall alpha beta, compare alpha beta = Eq -> 
+Lemma compare_Eq : forall (alpha beta : T2), compare alpha beta = Eq -> 
                                          alpha = beta.
 Proof.
   intros alpha beta; destruct (compare_correct alpha beta); trivial;
@@ -845,7 +846,7 @@ Proof.
     eapply lt_trans;eauto with T2.
 Qed.
 
-Lemma compare_rw_eq  alpha beta:  alpha = beta ->
+Lemma compare_rw_eq (alpha beta : T2):  alpha = beta ->
                                   compare alpha beta = Eq.
   intros; subst beta; generalize (compare_reflect alpha alpha);
     case (compare alpha alpha); trivial.
@@ -3682,8 +3683,9 @@ Module G0.
   Class G0 := mkg0 {vnf : T2; vnf_ok : nfb vnf}.
 
   Definition lt (alpha beta : G0) := T2.lt (@vnf alpha) (@vnf beta).
-
-  Definition compare alpha beta := compare (@vnf alpha) (@vnf beta).
+  
+  Instance compare_G0 : Compare G0 :=
+    fun alpha beta => compare (@vnf alpha) (@vnf beta).
 
   (* end snippet G0b *)
 
@@ -3719,18 +3721,18 @@ Module G0.
   (*||*)
   (* end snippet ltWf *)
 
-  Lemma compare_correct alpha beta :
-    CompareSpec (alpha = beta) (lt alpha beta) (lt beta alpha)
-                (compare alpha beta).
-  Proof.
-    destruct alpha, beta; cbn.
-    destruct (compare_correct vnf0 vnf1);subst. 
-    unfold compare; simpl.
-    -  rewrite compare_rw_eq; auto.
-       + constructor 1; f_equal; apply nfb_proof_unicity.
-    - unfold compare; rewrite compare_rw_lt; auto.
-    - unfold compare; rewrite compare_rw_gt; auto.
-  Qed. 
+Lemma compare_correct alpha beta :
+  CompareSpec (alpha = beta) (lt alpha beta) (lt beta alpha)
+              (compare alpha beta).
+Proof.
+  destruct alpha, beta; cbn.
+  destruct (compare_correct vnf0 vnf1);subst. 
+  unfold compare,compare_G0; simpl.
+  -  rewrite compare_rw_eq; auto.
+   + constructor 1; f_equal; apply nfb_proof_unicity.
+  - unfold compare,compare_G0; rewrite compare_rw_lt; auto.
+  - unfold compare,compare_G0; rewrite compare_rw_gt; auto.
+Qed. 
 
   Instance zero : G0.
   Proof.
diff --git a/theories/ordinals/Hydra/Omega2_Small.v b/theories/ordinals/Hydra/Omega2_Small.v
index bfc3fd65..ab1d44e2 100644
--- a/theories/ordinals/Hydra/Omega2_Small.v
+++ b/theories/ordinals/Hydra/Omega2_Small.v
@@ -21,7 +21,7 @@ Section Impossibility_Proof.
   
   Variable m : Hydra -> ON_Omega2.t.
   Context
-    (Hvar: @Hvariant _ _ (ON_Generic.wf (ON:=Omega2)) free m).
+    (Hvar: @Hvariant _ _ (ON_Generic.ON_wf (ON:=Omega2)) free m).
 
   (* end snippet Impossibilitya *)
 
@@ -172,7 +172,7 @@ Section Impossibility_Proof.
   Proof. (* .no-out *)
     unfold small_h;
     pattern (m big_h);
-      apply  well_founded_induction with (R := ON_lt) (1:= wf);
+      apply  well_founded_induction with (R := ON_lt) (1:= ON_wf);
       intros (i,j) IHij.
 
     (* end snippet mGe *)
diff --git a/theories/ordinals/OrdinalNotations/Example_3PlusOmega.v b/theories/ordinals/OrdinalNotations/Example_3PlusOmega.v
index 4f21f972..aa52f9a9 100644
--- a/theories/ordinals/OrdinalNotations/Example_3PlusOmega.v
+++ b/theories/ordinals/OrdinalNotations/Example_3PlusOmega.v
@@ -12,7 +12,7 @@ Definition O3O  :=  ON_plus (FinOrd 3) Omega.
 Existing Instance O3O.
 
 Arguments ON_t : clear implicits.
-Arguments ON_t {A lt compare} _.
+Arguments ON_t {A lt cmp} _.
 
 
 Program Definition f (z: ON_t O3O) : ON_t Omega :=
diff --git a/theories/ordinals/OrdinalNotations/ON_Finite.v b/theories/ordinals/OrdinalNotations/ON_Finite.v
index 9f4ee92e..6b0261a6 100644
--- a/theories/ordinals/OrdinalNotations/ON_Finite.v
+++ b/theories/ordinals/OrdinalNotations/ON_Finite.v
@@ -43,13 +43,11 @@ Abort.
 
 (* begin snippet compareDef:: no-out *)
 
-Definition compare {n:nat} (alpha beta : t n) :=
-  Nat.compare (proj1_sig alpha) (proj1_sig beta).
- 
+#[global] Instance compare_t {n:nat} : Compare (t n) :=
+  fun (alpha beta : t n) => Nat.compare (proj1_sig alpha) (proj1_sig beta).
 
 Lemma compare_correct {n} (alpha beta : t n) :
-  CompareSpec (alpha = beta) (lt alpha beta) (lt beta alpha)
-              (compare alpha beta).
+  CompSpec eq lt alpha beta (compare alpha beta).
 (* end snippet compareDef *)
 
 Proof.
@@ -68,10 +66,10 @@ Proof.
       destruct y, (x0 <? S n); auto; right; discriminate.    
      (* ... *)
 (* end snippet compareCorrectd *)
-    +  rewrite Nat.compare_lt_iff;  constructor 2.
-       destruct x0; [  lia |  apply leb_correct; lia].
-    +   rewrite Nat.compare_gt_iff; constructor 3.
-        destruct x; [lia | apply leb_correct; lia].
+    + rewrite Nat.compare_lt_iff;  constructor 2.
+      simpl; destruct x0; [  lia |  apply leb_correct; lia].
+    + rewrite Nat.compare_gt_iff; constructor 3.
+      simpl; destruct x; [lia | apply leb_correct; lia].
 Qed.
 
 Lemma compare_reflect {n:nat} (alpha beta : t  n) :
diff --git a/theories/ordinals/OrdinalNotations/ON_Generic.v b/theories/ordinals/OrdinalNotations/ON_Generic.v
index 4a446689..33634cf1 100644
--- a/theories/ordinals/OrdinalNotations/ON_Generic.v
+++ b/theories/ordinals/OrdinalNotations/ON_Generic.v
@@ -21,26 +21,23 @@ Local Open Scope ON_scope.
 *)
 
 (* begin snippet ONDef *)
-Class ON {A:Type}(lt: relation A)
-      (compare: A -> A -> comparison) :=
+Class ON {A:Type} (lt: relation A) (cmp: Compare A) :=
   {
-  comp :> Comparable lt compare;
-  wf : well_founded lt;
+  ON_comp :> Comparable lt cmp;
+  ON_wf : well_founded lt;
   }.
 (* end snippet ONDef *)
 
 (* begin snippet ONDefsa:: no-out  *)
 Section Definitions.
-  
-  Context  {A:Type}{lt : relation A}
-           {compare : A -> A -> comparison}
-           {on : ON lt compare}.
+
+  Context {A:Type} {lt : relation A} {cmp : Compare A} {on: ON lt cmp}.
   
   #[using="All"]
    Definition ON_t := A.
 
   #[using="All"]
-   Definition ON_compare := compare.
+   Definition ON_compare : A -> A -> comparison := compare.
 
   #[using="All"]
    Definition ON_lt := lt.
@@ -60,7 +57,7 @@ Section Definitions.
   Proof.
     intro x; eapply Acc_incl  with (fun x y =>  ON_lt (m x) (m  y)).
     - intros y z H; apply H.
-    - eapply Acc_inverse_image, wf.
+    - eapply Acc_inverse_image, ON_wf.
   Qed.
 
   (* begin snippet ONDefsb *)
@@ -315,7 +312,7 @@ Section SubON_properties.
   Lemma SubON_least : forall a ,  Least a  <-> Least (f a).
   Proof.
     split; intro H.
-    - intros y; destruct (compare_correct (f a) y).
+    - intros y; destruct (comparable_comp_spec (f a) y).
       + subst y; right.
       + now  left.
       + exfalso.
@@ -329,7 +326,7 @@ Section SubON_properties.
           apply (StrictOrder_Irreflexive a).
           auto.
         }
-    - intro x; destruct (compare_correct a x).
+    - intro x; destruct (comparable_comp_spec a x).
       subst; right.
       + now left.
       + apply SubON_mono in H0; specialize (H (f x)).
diff --git a/theories/ordinals/OrdinalNotations/ON_O.v b/theories/ordinals/OrdinalNotations/ON_O.v
index 3292046b..a3fed141 100644
--- a/theories/ordinals/OrdinalNotations/ON_O.v
+++ b/theories/ordinals/OrdinalNotations/ON_O.v
@@ -13,16 +13,16 @@ Coercion is_true: bool >-> Sortclass.
 Generalizable Variables A Lt comp.
 
 Section OA_given.
-  
+
   Context {A:Type}
           {Lt Le: relation A}
-          {compareA: A -> A -> comparison}
-          `(OA : ON A Lt compareA).
+          {cmpA: Compare A}
+          (OA : ON Lt cmpA).
 
 (** The type of ordinals less than [a] *)
 
 
-Definition t (a:A) := {b:A | compareA b a = Datatypes.Lt}.
+Definition t (a:A) := {b:A | compare b a = Datatypes.Lt}.
 
 Definition lt {a:A} : relation (t a) :=
   fun alpha beta => ON_lt (proj1_sig alpha) (proj1_sig beta).
@@ -30,22 +30,24 @@ Definition lt {a:A} : relation (t a) :=
 Definition le {a:A} : relation (t a) :=
   clos_refl (t a) lt.
 
-Definition compare {a:A} (alpha beta : t a) :=
-  compareA (proj1_sig alpha) (proj1_sig beta).
+#[global]
+Instance compare_t {a:A} : Compare (t a) :=
+fun (alpha beta : t a) =>
+  compare (proj1_sig alpha) (proj1_sig beta).
 
 Lemma compare_correct {a} (alpha beta : t a) :
-  CompareSpec (alpha = beta) (lt alpha beta) (lt beta alpha)
-              (compare alpha beta).
+  CompSpec eq lt alpha beta (compare alpha beta).
 Proof.
-  - destruct alpha, beta; unfold compare; cbn.
-    case_eq (compareA x x0); unfold lt; cbn.
+ unfold CompSpec, compare.
+  - destruct alpha, beta; unfold compare,compare_t; cbn.
+    case_eq (compare x x0); unfold lt; cbn.
     + constructor 1.
-      destruct (compare_correct x x0); try discriminate.
+      destruct (comparable_comp_spec x x0); try discriminate.
        subst; f_equal; apply eq_proofs_unicity_on.
        decide equality.
     + constructor 2.
-        destruct (compare_correct x x0); trivial; try discriminate.
-    + constructor 3; destruct (compare_correct x x0); trivial; discriminate.
+        destruct (comparable_comp_spec x x0); trivial; try discriminate.
+    + constructor 3; destruct (comparable_comp_spec x x0); trivial; discriminate.
 Qed.
 
 
@@ -64,14 +66,15 @@ Qed.
 Lemma lt_wf (a:A) : well_founded (@lt a).
 Proof.
   intro x;  unfold lt; apply Acc_inverse_image.
-   destruct x; cbn; apply wf.
+   destruct x; cbn; apply ON_wf.
 Qed.
 
 #[global] Instance sto a : StrictOrder (@lt a).
 Proof.
   destruct OA; split.
    - intro x; red;  unfold lt; destruct x; cbn.
-     intro; destruct sto; apply (StrictOrder_Irreflexive x); auto. 
+     destruct ON_comp.
+     intro; destruct comparable_sto; apply (StrictOrder_Irreflexive x); auto. 
    -   red; intros; unfold lt in *; destruct x,y,z; cbn in *.
        specialize (StrictOrder_Transitive x x0 x1).
        intro; auto.
diff --git a/theories/ordinals/OrdinalNotations/ON_Omega.v b/theories/ordinals/OrdinalNotations/ON_Omega.v
index 6b880a50..b08dbe8f 100644
--- a/theories/ordinals/OrdinalNotations/ON_Omega.v
+++ b/theories/ordinals/OrdinalNotations/ON_Omega.v
@@ -8,9 +8,12 @@ From hydras Require Import Schutte.
 
 Import Relations RelationClasses.
 
+#[global]
+Instance compare_nat : Compare nat := Nat.compare.
+
 (* begin snippet OmegaDefa:: no-out *)
 #[global]
- Instance Omega_comp : Comparable Peano.lt  Nat.compare.
+ Instance Omega_comp : Comparable Peano.lt compare_nat.
 Proof.
   split.
   - apply Nat.lt_strorder.
@@ -18,7 +21,7 @@ Proof.
 Qed.
 
 #[global]
- Instance Omega : ON Peano.lt Nat.compare.
+ Instance Omega : ON Peano.lt compare_nat.
 Proof.
  split.
  - apply Omega_comp.
@@ -67,7 +70,7 @@ Proof.
   - apply finite_lt_omega.
   - intros beta Hbeta; destruct (lt_omega_finite Hbeta) as [i Hi].
     exists i; now subst.
-  -  intros n p; destruct (Nat.compare_spec n p).
+  -  intros n p; unfold compare_nat; destruct (Nat.compare_spec n p).
      + now subst.
      + now apply finite_mono.
      + now apply finite_mono.
diff --git a/theories/ordinals/OrdinalNotations/ON_Omega2.v b/theories/ordinals/OrdinalNotations/ON_Omega2.v
index bd3288d6..958f08aa 100644
--- a/theories/ordinals/OrdinalNotations/ON_Omega2.v
+++ b/theories/ordinals/OrdinalNotations/ON_Omega2.v
@@ -12,9 +12,13 @@ Import Relations ON_Generic.
 Open Scope ON_scope.
 
 (* begin snippet Omega2Def:: no-out *)
-Instance Omega2: ON _ _ := ON_mult Omega Omega.
 
-Definition t := ON_t.  
+Instance compare_nat_nat : Compare t :=
+ compare_t compare_nat compare_nat.
+
+Instance Omega2: ON _ compare_nat_nat := ON_mult Omega Omega.
+
+Definition t := ON_t.
 
 Example ex1 : (5,8) o< (5,10).
 Proof.
@@ -128,14 +132,21 @@ Lemma compare_reflect alpha beta :
   | Gt => beta o< alpha
   end.
 Proof.
-  destruct alpha, beta; cbn; unfold ON_compare.  
-  destruct (compare_correct (n,n0) (n1,n2)); auto.
+  destruct alpha, beta; cbn; unfold ON_compare.
+  destruct (comparable_comp_spec (n,n0) (n1,n2)).
+  - rewrite H, compare_refl; reflexivity.
+  - apply compare_lt_iff in H.
+    rewrite H.
+    apply compare_lt_iff.
+    assumption.
+  - apply compare_gt_iff in H.
+    rewrite H.
+    apply compare_gt_iff.
+    assumption.
 Qed.
 
-
 Lemma compare_correct alpha beta :
-    CompareSpec (alpha = beta) (ON_lt alpha beta) (ON_lt beta alpha)
-                (ON_compare alpha beta).
+    CompSpec eq ON_lt alpha beta (ON_compare alpha beta).
 Proof.
   generalize (compare_reflect alpha beta).
   destruct (ON_compare alpha beta); now constructor. 
diff --git a/theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v b/theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v
index 496c42af..f67696b1 100644
--- a/theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v
+++ b/theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v
@@ -3,7 +3,7 @@
 
 
 From Coq Require Import Arith Compare_dec Lia.
-From hydras Require Import Simple_LexProd ON_Generic
+From hydras Require Import Comparable Simple_LexProd ON_Generic
         ON_plus ON_Omega.
 
 Import Relations.
@@ -14,7 +14,11 @@ Open Scope opo_scope.
 
 (* begin snippet OmegaPlusOmegaDef *)
 
-Instance Omega_plus_Omega: ON _ _ :=  ON_plus Omega Omega.
+Instance compare_nat_nat : Compare t :=
+ compare_t compare_nat compare_nat.
+
+Instance Omega_plus_Omega: ON _ compare_nat_nat :=
+ ON_plus Omega Omega.
 
 Definition t := ON_t.
 
@@ -377,7 +381,7 @@ Lemma Omega_as_lub  :
    forall alpha, 
      (forall i,  fin i o< alpha) <-> omega o<= alpha.
  Proof.
-   intro alpha; destruct (Comparable.compare_correct  omega alpha).
+   intro alpha; destruct (comparable_comp_spec omega alpha).
    - subst;split.
      +  right.
      + intros; constructor.
diff --git a/theories/ordinals/OrdinalNotations/ON_mult.v b/theories/ordinals/OrdinalNotations/ON_mult.v
index 89550f7f..f048e137 100644
--- a/theories/ordinals/OrdinalNotations/ON_mult.v
+++ b/theories/ordinals/OrdinalNotations/ON_mult.v
@@ -6,7 +6,7 @@
  
 From Coq Require Import Arith Compare_dec Lia 
      Relation_Operators RelationClasses.
-From hydras Require Import Simple_LexProd ON_Generic.
+From hydras Require Import Comparable Simple_LexProd ON_Generic.
 
 Import Relations.
 Generalizable All Variables.
@@ -25,19 +25,20 @@ Coercion is_true: bool >-> Sortclass.
 Section Defs.
 
   Context `(ltA: relation A)
-          (compareA : A -> A -> comparison)
-          (NA: ON ltA compareA)
+          (cmpA : Compare A)
+          (NA: ON ltA cmpA)
           `(ltB : relation B) 
-          (compareB : B -> B -> comparison)
-          (NB: ON ltB compareB).
+          (cmpB : Compare B)
+          (NB: ON ltB cmpB).
 
   Definition t := (B * A)%type.
   Definition lt : relation t := lexico ltB ltA.
   Definition le := clos_refl _ lt. 
 
-  Definition compare (alpha beta: t) : comparison :=
-    match compareB (fst alpha) (fst beta) with
-    | Eq => compareA (snd alpha) (snd beta)
+  #[global] Instance compare_t : Compare t :=
+    fun (alpha beta: t) =>
+    match compare (fst alpha) (fst beta) with
+    | Eq => compare (snd alpha) (snd beta)
     | c => c
     end.
    (*||*)
@@ -55,8 +56,7 @@ Section Defs.
   
 
   Lemma lt_wf : well_founded lt.
-  Proof. apply wf_lexico; apply wf. Qed.
-
+  Proof. apply wf_lexico; apply ON_wf. Qed.
 
   Lemma compare_reflect alpha beta :
     match (compare alpha beta)
@@ -66,9 +66,9 @@ Section Defs.
     | Gt => lt beta  alpha
     end.
   Proof.
-    destruct alpha, beta; cbn. unfold compare; cbn.
-    destruct (compare_correct b b0).
-    - subst; destruct (compare_correct a a0).
+    destruct alpha, beta; cbn. unfold compare, compare_t; cbn.
+    destruct (comparable_comp_spec b b0).
+    - subst; destruct (comparable_comp_spec a a0).
       + now subst.
       + now constructor 2.
       + now constructor 2.
@@ -78,8 +78,7 @@ Section Defs.
 
 
   Lemma compare_correct alpha beta :
-    CompareSpec (alpha = beta) (lt alpha beta) (lt beta alpha)
-                (compare alpha beta).
+    CompSpec eq lt alpha beta (compare alpha beta).
   Proof.
     generalize (compare_reflect alpha beta);
       destruct (compare alpha beta); now constructor. 
@@ -87,7 +86,7 @@ Section Defs.
 
   (* begin snippet multComp:: no-out *)
 
-  #[global] Instance mult_comp:  Comparable lt compare. 
+  #[global] Instance mult_comp:  Comparable lt compare_t.
   (* end snippet multComp *)
 
   Proof.
@@ -97,7 +96,7 @@ Section Defs.
   Qed. 
 
   (* begin snippet ONMult:: no-out *)
-  #[global] Instance ON_mult: ON lt compare.
+  #[global] Instance ON_mult: ON lt compare_t.
   (* end snippet ONMult *)
 
   Proof.
@@ -124,9 +123,9 @@ End Defs.
 (* end snippet endDefs *)
 
 
-Arguments lt_eq_lt_dec {A ltA compareA} _ {B ltB compareB} _.
-Arguments ON_mult {A ltA  compareA} _ {B ltB compareB}.
-Arguments lt_strorder {A} {ltA} {compareA} _  {B} {ltB} {compareB} _.
+Arguments lt_eq_lt_dec {A ltA cmpA} _ {B ltB cmpB} _.
+Arguments ON_mult {A ltA cmpA} _ {B ltB cmpB}.
+Arguments lt_strorder {A} {ltA} {cmpA} _  {B} {ltB} {cmpB} _.
 
 
 
diff --git a/theories/ordinals/OrdinalNotations/ON_plus.v b/theories/ordinals/OrdinalNotations/ON_plus.v
index 56612182..bb1be887 100644
--- a/theories/ordinals/OrdinalNotations/ON_plus.v
+++ b/theories/ordinals/OrdinalNotations/ON_plus.v
@@ -16,11 +16,11 @@ Coercion is_true: bool >-> Sortclass.
 Section Defs.
 
   Context `(ltA: relation A)
-          (compareA : A -> A -> comparison)
-          (NA: ON ltA  compareA).
+          (cmpA : Compare A)
+          (NA: ON ltA cmpA).
   Context `(ltB: relation B)
-          (compareB : B -> B -> comparison)
-          (NB: ON ltB compareB).
+          (cmpB : Compare B)
+          (NB: ON ltB cmpB).
 
   Definition t := (A + B)%type.
   Arguments inl  {A B} _.
@@ -30,11 +30,12 @@ Section Defs.
 (* end snippet Defs *)
 
 (* begin snippet compareDef *)
-Definition compare (alpha beta: t) : comparison :=
+#[global] Instance compare_t : Compare t :=
+fun (alpha beta: t) =>
    match alpha, beta with
      inl _, inr _ => Lt
-   | inl a, inl a' => compareA a a'
-   | inr b, inr b' => compareB b b'
+   | inl a, inl a' => compare a a'
+   | inr b, inr b' => compare b b'
    | inr _, inl _ => Gt
   end.
 (* end snippet compareDef *)
@@ -69,15 +70,14 @@ Lemma compare_reflect alpha beta :
   | Gt => lt beta  alpha
   end.
   destruct alpha, beta; cbn; auto.
-  destruct (compare_correct a a0); (now subst || constructor; auto).
-   - destruct (compare_correct b b0); (now subst || constructor; auto).
+  destruct (comparable_comp_spec a a0); (now subst || constructor; auto).
+   - destruct (comparable_comp_spec b b0); (now subst || constructor; auto).
 Qed.
 
 (* begin snippet compareCorrect:: no-out  *)
 
 Lemma compare_correct alpha beta :
-    CompareSpec (alpha = beta) (lt alpha beta) (lt beta alpha)
-                (compare alpha beta). (* .no-out *)
+    CompSpec eq lt alpha beta (compare alpha beta). (* .no-out *)
 (* end snippet compareCorrect *)
 
 Proof.
@@ -88,7 +88,7 @@ Qed.
 
 (* begin snippet plusComp:: no-out *)
 
-#[global] Instance plus_comp : Comparable lt compare.
+#[global] Instance plus_comp : Comparable lt compare_t.
 Proof.
   split.
   - apply lt_strorder.
@@ -105,8 +105,9 @@ Qed.
 
 
 Lemma lt_wf : well_founded lt.
-Proof. destruct NA, NB.
-       apply wf_disjoint_sum; [apply wf | apply wf0].
+Proof.
+  destruct NA, NB.
+  apply wf_disjoint_sum; [apply ON_wf | apply ON_wf0].
 Qed.
 
 (*||*)
@@ -119,7 +120,7 @@ Qed.
 .. coq:: no-out 
 |*)
 
-#[global] Instance ON_plus : ON lt compare.
+#[global] Instance ON_plus : ON lt compare_t.
 Proof.
   split.
   - apply plus_comp.
@@ -144,8 +145,8 @@ Defined.
 
 End Defs.
 
-Arguments lt_eq_lt_dec {A ltA compareA} _ {B ltB  compareB} _.
-Arguments ON_plus {A ltA compareA} _ {B ltB  compareB}.
+Arguments lt_eq_lt_dec {A ltA cmpA} _ {B ltB  cmpB} _.
+Arguments ON_plus {A ltA cmpA} _ {B ltB cmpB}.
 
 
 
diff --git a/theories/ordinals/OrdinalNotations/OmegaOmega.v b/theories/ordinals/OrdinalNotations/OmegaOmega.v
index 4de44bc0..cc9e2169 100644
--- a/theories/ordinals/OrdinalNotations/OmegaOmega.v
+++ b/theories/ordinals/OrdinalNotations/OmegaOmega.v
@@ -93,7 +93,8 @@ Module LO.
   Qed.
 
   (* begin snippet compareDef:: no-out  *)
-  Fixpoint compare (alpha beta:t):comparison :=
+  Instance compare_t : Compare t :=
+  fix cmp (alpha beta:t) :=
     match alpha, beta with
     | nil, nil => Eq
     | nil, ocons a' n' b' => Lt
@@ -103,14 +104,14 @@ Module LO.
        | Lt => Lt
        | Gt => Gt
        | Eq => (match Nat.compare n n' with
-                | Eq => compare b b'
+                | Eq => cmp b b'
                 | comp => comp
                 end)
        end)
     end.
   
   Lemma compare_ref (alpha beta:t) :
-    compare alpha beta = T1.compare (refine alpha) (refine beta).
+    compare alpha beta = compare (refine alpha) (refine beta).
  (* end snippet compareDef  *)  
   Proof.
     revert beta. induction alpha.
@@ -126,12 +127,12 @@ Module LO.
   Qed.
 
   (* begin snippet ltDef *)
-  Definition lt alpha beta : Prop :=
+  Definition lt (alpha beta : t) : Prop :=
     compare alpha beta = Lt.
   (* end snippet ltDef *)
   
   Lemma compare_rev :
-    forall alpha beta,
+    forall (alpha beta : t),
       compare beta alpha = CompOpp (compare alpha beta).
   Proof.
     induction alpha,  beta.
@@ -144,6 +145,7 @@ Module LO.
         destruct  (Nat.compare n2 n0) eqn:? ; now cbn.
   Qed.
 
+  
 
   Lemma compare_reflect :
     forall alpha beta,
@@ -166,18 +168,41 @@ Module LO.
             subst; try easy;
               apply Nat.compare_eq_iff in Heq as -> ;
               destruct (n ?= n0) eqn:Heqc; trivial.
-        * now apply Nat.compare_eq_iff in Heqc as ->.
+        * destruct (compare _ _) eqn: H.
+          apply Nat.compare_eq_iff in Heqc as ->.
+          rewrite IHalpha.
+          reflexivity.
+          reflexivity.
+          rewrite Nat.compare_antisym.
+          rewrite Heqc.
+          reflexivity.
         * destruct (n ?= n0) eqn:Heqn; trivial;
             now rewrite Nat.compare_antisym, Heqn.
-        * rewrite Nat.compare_antisym;   now rewrite Heqc.
+        * destruct (compare _ _) eqn: H.
+          apply Nat.compare_eq_iff in Heqc as ->.
+          rewrite IHalpha.
+          reflexivity.
+          reflexivity.
+          rewrite Nat.compare_antisym.
+          rewrite Heqc.
+          reflexivity.
         * destruct (n ?= n0) eqn:?; trivial; try discriminate.
           rewrite Nat.compare_antisym; now rewrite Heqc0.
-        *  rewrite Nat.compare_antisym; now rewrite Heqc.
+        * destruct (compare _ _) eqn: H.
+          apply Nat.compare_eq_iff in Heqc as ->.
+          rewrite IHalpha.
+          reflexivity.
+          reflexivity.
+          rewrite Nat.compare_antisym.
+          rewrite Heqc.
+          reflexivity.
+        * rewrite Nat.compare_antisym.
+          rewrite Heqc.
+          reflexivity.
   Qed.
 
   Lemma compare_correct (alpha beta: t):
-    CompareSpec (alpha = beta) (lt alpha beta) (lt beta alpha)
-                (compare alpha beta).
+    CompSpec eq lt alpha beta (compare alpha beta).
   Proof.
     unfold lt;  generalize (compare_reflect alpha beta).
     destruct (compare alpha beta); now constructor.
@@ -479,7 +504,8 @@ Module OO.
 
   Definition lt (alpha beta: OO) := LO.lt (data alpha) (data beta).
   Definition le := leq lt.
-  Definition compare (alpha beta: OO):= LO.compare (data alpha) (data beta).
+  Instance compare_OO : Compare OO := 
+    fun (alpha beta: OO) => LO.compare_t (data alpha) (data beta).
   (*  end snippet OODef *)
 
   Instance Zero : OO := @mkord nil refl_equal.
@@ -577,11 +603,26 @@ Module OO.
   Proof.
     split.
     - apply oo_str.
-    - destruct a, b; unfold compare; cbn.
-      destruct (LO.compare_correct data0 data1).
-      + constructor; subst; apply OO_eq_intro; now cbn.
-      + constructor; red; now cbn.
-      + constructor; red; now cbn.
+    - destruct a, b; cbn.
+      destruct (comparable_comp_spec data0 data1).
+      + subst.
+        assert (compare_t data1 data1 = compare data1 data1) by reflexivity.
+        rewrite H.
+        rewrite compare_refl.
+        constructor.
+        apply OO_eq_intro; now cbn.
+      + apply compare_lt_iff in H.
+        unfold compare in H.
+        rewrite H.
+        constructor; red; now cbn.
+      + apply compare_gt_iff in H.
+        unfold compare in H.
+        rewrite H.
+        constructor; red.
+        apply compare_gt_iff.
+        unfold compare.
+        simpl.
+        assumption.
   Qed. 
 
   (* begin snippet ltWf:: no-out *)
diff --git a/theories/ordinals/Prelude/Comparable.v b/theories/ordinals/Prelude/Comparable.v
index 6d3dcd34..8db14e7d 100644
--- a/theories/ordinals/Prelude/Comparable.v
+++ b/theories/ordinals/Prelude/Comparable.v
@@ -1,24 +1,23 @@
 From Coq Require Import Relations RelationClasses Setoid.
 Require Export MoreOrders.
 
-
 (* begin snippet ComparableDef *)
-Class Comparable {A:Type} 
-  (lt: relation A)
-  (compare : A -> A -> comparison) :=
-  {
-  sto :> StrictOrder lt;
-  compare_correct: forall a b,
-      CompareSpec (a = b) (lt a b) (lt b a) (compare a b);
-  }.
+Class Compare (A:Type) := compare : A -> A -> comparison.
+
+Class Comparable {A:Type} (lt: relation A) (cmp : Compare A) := {
+  comparable_sto :> StrictOrder lt;
+  comparable_comp_spec : forall a b, CompSpec eq lt a b (compare a b);
+}.
 (* end snippet ComparableDef *)
 
+#[export] Hint Mode Compare ! : typeclass_instances.
+#[export] Hint Mode Comparable ! - - : typeclass_instances.
+
 Section Comparable.
 
   Context {A: Type}
           {lt: relation A}
-          {compare : A -> A -> comparison}
-          {comparable : Comparable lt compare}.
+          {cmp: Compare A} `{!Comparable lt cmp}.
   #[local] Notation le := (leq lt). 
 
   #[deprecated(note="use StrictOrder_Transitive")]
@@ -43,44 +42,11 @@ Section Comparable.
     - now apply lt_not_gt in Hlt.
     - subst; now apply StrictOrder_Irreflexive in Hlt.
   Qed.
-
-  #[using="All"]
-  Definition lt_b (a b: A): bool :=
-    match compare a b with
-    | Lt => true
-    | _ => false
-    end.
-
-  Lemma lt_b_iff (a b: A):
-    lt_b a b = true <-> lt a b.
-  Proof.
-    unfold lt_b.
-    pose proof (compare_correct a b) as [Heq | H | H];
-    split; intro; subst; try easy.
-    - now apply StrictOrder_Irreflexive  in H.
-    - now apply lt_not_gt in H.
-  Qed.
-
-  Lemma lt_b_false_iff (a b: A):
-    lt_b a b = false  <-> ~ lt a b.
-  Proof.
-     unfold lt_b.
-    pose proof (compare_correct a b) as [Heq | H | H];
-    split; intro; subst; try easy.
-    - apply StrictOrder_Irreflexive.   
-    - now apply lt_not_gt.
-  Qed.
-
-  Lemma lt_b_irrefl (a :A) :
-    lt_b a a = false.
-  Proof. 
-   rewrite lt_b_false_iff; apply StrictOrder_Irreflexive.   
-  Qed.
   
   Lemma compare_lt_iff (a b: A):
     compare a b = Lt <-> lt a b.
   Proof.
-    pose proof (compare_correct a b) as [Heq | H | H];
+    pose proof (comparable_comp_spec a b) as [Heq | H | H];
     split; intro; subst; try easy.
     - now apply StrictOrder_Irreflexive  in H.
     - now apply lt_not_gt in H.
@@ -101,28 +67,10 @@ Section Comparable.
     now apply compare_lt_iff, StrictOrder_Irreflexive in H.
   Qed.
 
-  (* Relation Eq *)
-  #[using="All"]
-  Definition eq_b (a b: A): bool :=
-    match compare a b with
-    | Eq => true
-    | _ => false
-    end.
-
-
-  Lemma eq_b_iff (a b: A):
-    eq_b a b = true <-> a = b.
-  Proof.
-    unfold eq_b.
-    pose proof (compare_correct a b) as [Heq | H | H];
-    split; intro; subst; try easy;
-    now apply StrictOrder_Irreflexive in H.
-  Qed.
-
   Lemma compare_eq_iff (a b: A):
     compare a b = Eq <-> a = b.
   Proof.
-    pose proof (compare_correct a b) as [Heq | H | H];
+    pose proof (comparable_comp_spec a b) as [Heq | H | H];
     split; intro; subst; try easy;
     now apply StrictOrder_Irreflexive in H.
   Qed.
@@ -131,7 +79,7 @@ Section Comparable.
   Lemma compare_refl (a: A):
     compare a a = Eq.
   Proof.
-    pose proof (compare_correct a a) as [H | H | H].
+    pose proof (comparable_comp_spec a a) as [H | H | H].
     1: reflexivity.
     all: now apply StrictOrder_Irreflexive in H.
   Qed.
@@ -149,7 +97,7 @@ Section Comparable.
   Lemma compare_gt_iff (a b: A):
     compare a b = Gt <-> lt b a.
   Proof.
-    pose proof (compare_correct a b) as [Heq | Hlt | Hgt];
+    pose proof (comparable_comp_spec a b) as [Heq | Hlt | Hgt];
     split; intro; subst; try easy.
     - now apply StrictOrder_Irreflexive in H.
     - now apply lt_not_gt in H.
@@ -191,31 +139,6 @@ Section Comparable.
     now apply lt_not_gt in Hgt.
   Qed.
 
-  (* Relation Le *)
-  #[using="All"]
-  Definition le_b (a b: A): bool :=
-    negb (lt_b b a).
-
-  Lemma le_b_iff (a b: A):
-    le_b a b = true <-> le a b.
-  Proof.
-    unfold le_b, negb, lt_b.
-    pose proof (compare_correct a b) as [Heq | Hlt | Hgt];
-    split; intro; subst; try easy.
-    - apply le_lt_eq; now right.
-    - now rewrite compare_refl.
-    - apply le_lt_eq; now left.
-    - now apply compare_gt_iff in Hlt as ->.
-    - apply compare_lt_iff in Hgt.
-      rewrite Hgt in H.
-      congruence.
-    - exfalso.
-      apply le_lt_eq in H as [Hlt | Heq].
-      * now apply lt_not_gt in Hgt.
-      * rewrite Heq in Hgt; now apply StrictOrder_Irreflexive in Hgt.
-  Qed.
-
-
   Lemma le_refl (a: A): le a a.
   Proof.
     apply le_lt_eq; now right.
@@ -305,15 +228,15 @@ Section Comparable.
     max a b = a \/ max a b = b.
   Proof.
     unfold max.
-    pose proof (compare_correct a b) as [Hab | Hab | Hab]; tauto.
+    pose proof (comparable_comp_spec a b) as [Hab | Hab | Hab]; tauto.
   Qed.
 
   Lemma max_comm (a b: A):
     max a b = max b a.
   Proof.
     unfold max.
-    pose proof (compare_correct a b) as [Hab | Hab | Hab];
-    pose proof (compare_correct b a) as [Hba | Hba | Hba].
+    pose proof (comparable_comp_spec a b) as [Hab | Hab | Hab];
+    pose proof (comparable_comp_spec b a) as [Hba | Hba | Hba].
     5,9: now apply lt_not_gt in Hab.
     all: easy.
   Qed.
@@ -327,7 +250,7 @@ Section Comparable.
     - apply compare_ge_iff in H as [Hlt | Heq].
       + now rewrite Hlt.
       + rewrite Heq. now apply compare_eq_iff in Heq.
-    - pose proof (compare_correct a b) as [Hab | Hab | Hab].
+    - pose proof (comparable_comp_spec a b) as [Hab | Hab | Hab].
       + subst. apply le_refl.
       + exfalso.
         apply compare_lt_iff in Hab.
@@ -342,7 +265,7 @@ Section Comparable.
       rewrite le_lt_eq, <- compare_lt_iff, <- compare_eq_iff.
     split; intro H.
     - now destruct H as [-> | ->].
-    - pose proof (compare_correct a b) as [Hab | Hab | Hab].
+    - pose proof (comparable_comp_spec a b) as [Hab | Hab | Hab].
       + now right.
       + now left.
       + exfalso.
@@ -361,7 +284,7 @@ Section Comparable.
   Lemma le_max_a (a b: A): le a (max a b).
   Proof.
     unfold max.
-    pose proof (compare_correct a b) as [Heq | Hlt | Hgt].
+    pose proof (comparable_comp_spec a b) as [Heq | Hlt | Hgt].
     1,3: subst; now apply le_refl.
     now apply lt_incl_le.
   Qed.
@@ -375,9 +298,9 @@ Section Comparable.
     max (max a b) c = max a (max b c).
   Proof.
     unfold max.
-    pose proof (compare_correct a b) as [Hab | Hab | Hab];
-    pose proof (compare_correct b c) as [Hbc | Hbc | Hbc];
-    pose proof (compare_correct a c) as [Hac | Hac | Hac];
+    pose proof (comparable_comp_spec a b) as [Hab | Hab | Hab];
+    pose proof (comparable_comp_spec b c) as [Hbc | Hbc | Hbc];
+    pose proof (comparable_comp_spec a c) as [Hac | Hac | Hac];
     subst; try rewrite compare_refl; try easy.
     - now apply lt_not_gt in Hbc.
     - now apply lt_not_gt in Hab.
@@ -407,15 +330,15 @@ Section Comparable.
     min a b = a <-> max a b = b.
   Proof.
     unfold min, max.
-    pose proof (compare_correct a b) as [Hab | Hab | Hab]; subst; easy.
+    pose proof (comparable_comp_spec a b) as [Hab | Hab | Hab]; subst; easy.
   Qed.
 
   Lemma min_comm (a b: A):
     min a b = min b a.
   Proof.
     unfold min.
-    pose proof (compare_correct a b) as [Hab | Hab | Hab];
-        pose proof (compare_correct b a) as [Hba | Hba | Hba].
+    pose proof (comparable_comp_spec a b) as [Hab | Hab | Hab];
+        pose proof (comparable_comp_spec b a) as [Hba | Hba | Hba].
         5,9: now apply lt_not_gt in Hab.
         all: easy.
   Qed.
@@ -456,7 +379,7 @@ Section Comparable.
     le (min a b) a.
   Proof.
     unfold min.
-    pose proof (compare_correct a b) as [Heq | Hlt | Hgt]; subst.
+    pose proof (comparable_comp_spec a b) as [Heq | Hlt | Hgt]; subst.
     1,2: now apply le_refl.
     now apply lt_incl_le.
   Qed.
@@ -473,9 +396,9 @@ Section Comparable.
   Proof.
     intros *.
     unfold min.
-    pose proof (compare_correct a b) as [Hab | Hab | Hab];
-    pose proof (compare_correct b c) as [Hbc | Hbc | Hbc];
-    pose proof (compare_correct a c) as [Hac | Hac | Hac];
+    pose proof (comparable_comp_spec a b) as [Hab | Hab | Hab];
+    pose proof (comparable_comp_spec b c) as [Hbc | Hbc | Hbc];
+    pose proof (comparable_comp_spec a c) as [Hac | Hac | Hac];
     subst; try rewrite compare_refl; try easy.
     - now apply lt_not_gt in Hbc.
     - now apply lt_not_gt in Hab.
@@ -513,14 +436,14 @@ Section Comparable.
     | Gt => lt b a
     end.
   Proof.
-    pose proof (compare_correct a b) as [Heq | Hlt | Hgt]; assumption.
+    pose proof (comparable_comp_spec a b) as [Heq | Hlt | Hgt]; assumption.
   Qed.
 
 
   Lemma lt_eq_lt:
     forall alpha beta, lt alpha  beta \/ alpha = beta \/ lt beta alpha.
   Proof.
-    intros; destruct (compare_correct alpha beta); auto.
+    intros; destruct (comparable_comp_spec alpha beta); auto.
   Qed.
 
   Definition lt_eq_lt_dec 
@@ -572,7 +495,7 @@ Tactic Notation "compare" "trans" constr(H1) constr(H2) "as" simple_intropattern
   compare_trans H1 H2 intropattern.
 
 Ltac compare_destruct_eqn a b H :=
-  destruct (_ a b) eqn: H;
+  destruct (compare a b) eqn: H;
   [ apply compare_eq_iff in H as <-
   | apply compare_lt_iff in H
   | apply compare_gt_iff in H
@@ -580,7 +503,3 @@ Ltac compare_destruct_eqn a b H :=
 
 Tactic Notation "compare" "destruct" constr(a) constr(b) "as" ident(H) :=
   compare_destruct_eqn a b H.
-
-
-
-
diff --git a/theories/ordinals/Prelude/DecPreOrder.v b/theories/ordinals/Prelude/DecPreOrder.v
index 696260c0..c9aa37f6 100644
--- a/theories/ordinals/Prelude/DecPreOrder.v
+++ b/theories/ordinals/Prelude/DecPreOrder.v
@@ -27,6 +27,21 @@ Notation EqDecision A := (RelDecision (@eq A)).
 Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
   if dec then true else false.
 
+Lemma bool_decide_eq_true (P : Prop) `{Decision P} : bool_decide P = true <-> P.
+Proof.
+  unfold bool_decide.
+  destruct H; intuition discriminate.
+Qed.
+
+Lemma bool_decide_eq_false (P : Prop) `{Decision P} : bool_decide P = false <-> ~P.
+Proof.
+  unfold bool_decide.
+  destruct H; intuition discriminate.
+Qed.
+
+Instance comparison_eq_dec : EqDecision comparison.
+Proof. intros c1 c2; unfold Decision; decide equality. Defined.
+
 Instance Total_Reflexive{A:Type}{R: relation A}(rt : Total R):
   Reflexive R.
 Proof. intros a ; now destruct (rt a a). Qed.
diff --git a/theories/ordinals/Prelude/First_toggle.v b/theories/ordinals/Prelude/First_toggle.v
index 4fa1a193..ae73e57f 100644
--- a/theories/ordinals/Prelude/First_toggle.v
+++ b/theories/ordinals/Prelude/First_toggle.v
@@ -7,28 +7,26 @@ Computes the first  [l]  between [n] and [p] (excluded) such that
 
 (** Pierre Castéran, Univ. Bordeaux and LaBRI *)
 
-
 From Coq Require Import Arith Lia.
+From hydras Require Import DecPreOrder.
 
 Section Hypos.
-  Variables (P : nat -> bool)
-            (n p : nat).
+  Context (P : nat -> Prop) `{Pdec: forall n, Decision (P n)} (n p : nat).
  
-  Hypotheses (Hnp : n < p)
-             (Hn : P n = true) (Hp : P p = false).
+  Hypotheses (Hnp : n < p) (Hn : P n) (Hp : ~ P p).
 
 (* begin hide *)
   
   Let  search_toggle  (delta : nat)(H : 0 < delta /\ delta <= p - n)
-             (invar : forall i, n <= i -> i <= p - delta -> P i = true) :
+             (invar : forall i, n <= i -> i <= p - delta -> P i) :
     {l : nat | n <= l  /\ l < p /\
-               (forall i: nat, n <= i -> i <= l -> P i = true ) /\ 
-               (P (S l ) = false)}.
+               (forall i: nat, n <= i -> i <= l -> P i) /\ 
+               (~ P (S l ))}.
   
   Proof.
     generalize delta H invar.
     clear delta H invar.
-    intro delta; pattern delta; apply well_founded_induction with lt.
+    intro delta; pattern delta; apply well_founded_induction with Nat.lt.
     apply lt_wf.
     
     intros d Hd.
@@ -38,12 +36,11 @@ Section Hypos.
     destruct H.
     elimtype False. inversion H. intros; subst.
     
-    case_eq (P (p - n0)). 
-    intro.
+    destruct (decide (P (p - n0))) as [H|H].
     destruct (Hd n0).
     auto with arith.
     destruct n0.
-    replace (p - 0) with p in H. rewrite Hp in H; discriminate.
+    replace (p - 0) with p in H. congruence.
     auto with arith.
     split; auto with arith.
     destruct H0; auto with arith.
@@ -71,7 +68,7 @@ Section Hypos.
   Remark R1 : 0 < delta /\ delta <= p - n.
   Proof.   unfold delta.  clear search_toggle; abstract lia.  Qed.
 
-  Remark R2 :  forall i, n <= i -> i <= p - delta -> P i = true.
+  Remark R2 :  forall i, n <= i -> i <= p - delta -> P i.
   Proof.
     clear search_toggle; unfold delta; intros; replace i with n; [trivial | lia].
   Qed.
@@ -80,8 +77,8 @@ Section Hypos.
   
   Definition first_toggle :
   {l : nat |  n <= l /\ l < p /\
-              (forall i : nat, n <= i -> i <= l -> P i = true) /\
-              P (S l) = false}.
+              (forall i : nat, n <= i -> i <= l -> P i) /\
+              ~ P (S l)}.
   (* begin hide *)
   Proof.
     exact  (search_toggle  (p-n) R1 R2).
diff --git a/theories/ordinals/Schutte/Correctness_E0.v b/theories/ordinals/Schutte/Correctness_E0.v
index e4c71687..ab142025 100644
--- a/theories/ordinals/Schutte/Correctness_E0.v
+++ b/theories/ordinals/Schutte/Correctness_E0.v
@@ -420,7 +420,7 @@ Proof with eauto with T1.
 
      + repeat rewrite inject_rw.
        simpl.
-       destruct (T1.compare alpha1 beta1) eqn:H1;
+       destruct (compare alpha1 beta1) eqn:H1;
        repeat rewrite inject_rw.
        * apply compare_eq_iff in H1 as <-.
           rewrite <- (case_Eq (inject alpha1) (inject alpha2)
diff --git a/theories/ordinals/solutions_exercises/lt_succ_le.v b/theories/ordinals/solutions_exercises/lt_succ_le.v
index d1eb414c..48acf99c 100644
--- a/theories/ordinals/solutions_exercises/lt_succ_le.v
+++ b/theories/ordinals/solutions_exercises/lt_succ_le.v
@@ -5,8 +5,8 @@ Section Proofs_of_lt_succ_le.
   
 Context (A:Type)
         (lt  : relation A)
-        (compare : A -> A -> comparison)
-        (On : ON lt compare).
+        (cmp : Compare A)
+        (On : ON lt cmp).
 
 Section Proofs.
   Variables alpha beta : A.
diff --git a/theories/ordinals/solutions_exercises/predSuccUnicity.v b/theories/ordinals/solutions_exercises/predSuccUnicity.v
index 950156fe..b441742f 100644
--- a/theories/ordinals/solutions_exercises/predSuccUnicity.v
+++ b/theories/ordinals/solutions_exercises/predSuccUnicity.v
@@ -5,8 +5,8 @@ Section Proofs_of_unicity.
   
 Context (A:Type)
         (lt le : relation A)
-        (compare : A -> A -> comparison)
-        (On : ON lt compare).
+        (cmp : Compare A)
+        (On : ON lt cmp).
 
 Section Proofs.
   Variables alpha beta : A.