diff --git a/doc/hydra-chapter.tex b/doc/hydra-chapter.tex
index c2ac8520..93cb1974 100644
--- a/doc/hydra-chapter.tex
+++ b/doc/hydra-chapter.tex
@@ -846,7 +846,7 @@ \subsection{Big steps}
 
 \input{movies/snippets/Hydra_Definitions/battleRelDef}
 
-The following property allows us to build battle rounds by composition of smaller ones.
+The following property allows us to build battles by composition of smaller ones.
 
 %% TODO display subgoals when fixed
 
diff --git a/doc/ordinal-chapter.tex b/doc/ordinal-chapter.tex
index 20e90d0f..268cfd99 100644
--- a/doc/ordinal-chapter.tex
+++ b/doc/ordinal-chapter.tex
@@ -46,8 +46,7 @@ \chapter{Introduction to ordinal numbers and ordinal notations}
 \item Dots : ``$\ldots$'' stand for  infinite sequences of ordinals, not shown for lack of space. For instance, the ordinal $42$ is not shown in the first line, but it exists, somewhere between $17$ and $\omega$.
 \item Each ordinal printed in black is the immediate successor of another ordinal. We call it a \emph{successor} ordinal. For instance, $12$ is the successor of $11$, and $\omega^4+1$ the successor of $\omega^4$.
 \item Ordinals (displayed in red)  that  follow immediately dots are called \emph{limit ordinals}. With respect to the order induced by this sequence, any limit ordinal $\alpha$ is the least upper bound of  the set $\mathbb{O}_\alpha$ of all ordinals strictly less than $\alpha$.
-\item
-For instance $\omega$ is the least upper bound of the set of all finite ordinals (in the first line). It is also the first limit ordinal, and the first infinite ordinal, in the sense that 
+For instance,$\omega$ is the least upper bound of the set of all finite ordinals (in the first line). It is also the first limit ordinal, and the first \emph{infinite ordinal number}, in the sense that 
 the set $\mathbb{O}_\omega$ is infinite.
 \item The ordinal $\epsilon_0$ is the first number which is equal to its own exponential of base $\omega$. It plays an important role in proof theory, and is particularly studied in chapters~\ref{chap:T1} to \ref{chap:alpha-large}.
 \item Any ordinal is  either the ordinal \textcolor{blue}{$0$},
@@ -59,6 +58,15 @@ \chapter{Introduction to ordinal numbers and ordinal notations}
 
 \section{The mathematical point of view}
 
+
+
+We cannot cite all the literature published on ordinals since Cantor's book
+\cite{cantorbook}, and 
+leave it to the reader to explore the bibliography.
+The introduction of Jos\'e Grimm's report~\cite{grimm:hal-00911710} contains also a nice presentation of the main properties of ordinals.
+
+For simplicity's sake, we will only give the definitions which are useful for understanding our \coq development.
+
 \subsection{Well-ordered sets}
 Let us start with some definitions.
 A  \emph{well-ordered set} is a set provided with a binary relation $<$ which has the following properties.
@@ -88,21 +96,15 @@ \subsection{Ordinal numbers}
 there exists a strictly monotonous bijection $b$ from $A$ to $B$, \emph{i.e.} which verifies the proposition
 $\forall x\,y\in A,\, x <_A y \Rightarrow b(x) <_B  b(y)$.
 
-Having the same order type is an equivalence relation between well-ordered sets. Ordinal numbers (in short: \emph{ordinals})  are descriptions (\emph{names}) of the equivalence classes.
+Having the same order type is an equivalence relation between well-ordered sets. Ordinal numbers (in short: \emph{ordinals})  are descriptions (\emph{names}) of the associated equivalence classes.
 For instance, the order type of $(\mathbb{N},<)$ is associated with the ordinal called  $\omega$, and the order we considered on 
-the disjoint union of $\mathbb{N}$ and itself is named $\omega+\omega$.
+the disjoint union of two copies of $\mathbb{N}$ is associated with  $\omega \times 2$ (a.k.a. $\omega+\omega$).
 
 In a set-theoretic framework, one can consider any ordinal $\alpha$ as a well-ordered set, whose  elements are just the ordinals strictly less than $\alpha$, \emph{i.e.} the \emph{segment} $\mathbb{O}_\alpha=[0, \alpha)$. So, one can speak about \emph{finite}, \emph{infinite}, \emph{countable}, etc., ordinals. Nevertheless, since we work within type theory, 
 we do not identify ordinals as sets of ordinals, but consider the correspondence between ordinals and sets of ordinals as the function that maps $\alpha$ to $\mathbb{O}_\alpha$.
 For instance $\mathbb{O}_\omega=\mathbb{N}$, and $\mathbb{O}_7=\{0,1,2,3,4,5,6\}$.
 
 
-We cannot cite all the literature published on ordinals since Cantor's book
-\cite{cantorbook}, and 
-leave it to the reader to explore the bibliography.
-
-The introduction of Jos\'e Grimm's report~\cite{grimm:hal-00911710} contains a nice presentation of the main properties of ordinals.
-
 
 \section{Ordinal numbers in Coq}
 
@@ -139,7 +141,7 @@ \section{Ordinal Notations}
 Fortunately, the ordinals we need for  studying hydra battles are much simpler than Schütte's, and can be represented as quite simple data types in \gallina. 
 
 Let $\alpha$ be some (countable) ordinal; 
-in \coq{} terms, we call \emph{ordinal notation for $\alpha$} a structure composed 
+we call \emph{ordinal notation for $\alpha$} any structure composed 
 of:
 \begin{itemize}
 \item A data type $A$ for representing all ordinals strictly below $\alpha$,
@@ -163,7 +165,7 @@ \subsubsection{The \texttt{Comparable} class}
 
 The \texttt{Comparable} class, contributed by Jérémy Damour and Théo Zimmermann, 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} as specialized by \texttt{Datatypes.CompSpec}.
+\texttt{Datatypes.CompareSpec} and predicate \texttt{Datatypes.CompSpec}.
 
 \begin{Coqsrc}
   Inductive CompareSpec (Peq Plt Pgt : Prop) :
@@ -291,13 +293,16 @@ \section{Sum of  two ordinal notations}
 Standard library's lemma \texttt{Wellfounded.Disjoint\_Union.wf\_disjoint\_sum} 
 is applied  to prove that our order \texttt{lt} is well-founded, allowing us to build an instance of \texttt{ON}:
 
-\inputsnippets{ON_plus/ltWf, ON_plus/OnPlus}
+\inputsnippets{ON_plus/ltWf}
 
-\subsection{The ordinal \texorpdfstring{$\omega+\omega$}{omega + omega}}
+\inputsnippets{ON_plus/OnPlus}
+
+\subsection{Example: The ordinal \texorpdfstring{$\omega+\omega$}{omega + omega}}
 
 The ordinal $\omega+\omega$ (also known as $\omega\times 2$) may be represented as the concatenation 
 of two copies of $\omega$ (Figure~\ref{fig:omega-plus-omega}).
 It is also represented by the two first lines of Figure~\ref{fig:ordinal-sequence}.
+We define this notation in \coq{} as an instance of \texttt{ON\_plus}.
 
 \begin{figure}[h]
    \centering
@@ -324,7 +329,7 @@ \subsection{The ordinal \texorpdfstring{$\omega+\omega$}{omega + omega}}
    \label{fig:omega-plus-omega}
  \end{figure}
 
-We can define this notation in \coq{} as an instance of \texttt{ON\_plus}.
+
 
 
 \vspace{4pt}
@@ -523,7 +528,9 @@ \subsubsection{Addition}
 
 We can define on \texttt{Omega2} an addition which extends the addition on \texttt{nat}. Please note that this operation is not commutative:
 
-\inputsnippets{ON_Omega2/plusDef, ON_Omega2/plusExamples}
+\inputsnippets{ON_Omega2/plusDef}
+
+\inputsnippets{ON_Omega2/plusExamples}
 
 
 \subsubsection{Finite multiplication}
diff --git a/theories/ordinals/Hydra/Hydra_Definitions.v b/theories/ordinals/Hydra/Hydra_Definitions.v
index 409e8f5e..9961d471 100644
--- a/theories/ordinals/Hydra/Hydra_Definitions.v
+++ b/theories/ordinals/Hydra/Hydra_Definitions.v
@@ -497,7 +497,7 @@ Class Hvariant {A:Type}{Lt:relation A}
       (Wf: well_founded Lt)(B : Battle)
       (m: Hydra -> A): Prop :=
   {variant_decr: forall i h h',
-      h <> head -> battle_rel B i  h h' -> Lt (m h') (m h)}.
+      h <> head -> battle_rel B i h h' -> Lt (m h') (m h)}.
 
 (* end snippet HvariantDef *)
 
diff --git a/theories/ordinals/Hydra/Hydra_Lemmas.v b/theories/ordinals/Hydra/Hydra_Lemmas.v
index 90b191cc..b52a6eb1 100644
--- a/theories/ordinals/Hydra/Hydra_Lemmas.v
+++ b/theories/ordinals/Hydra/Hydra_Lemmas.v
@@ -206,10 +206,10 @@ Qed.
 (** ** Properties of [battle] *)
 
 (* begin snippet battleTrans *)
-Lemma rounds_trans {b:Battle} :
-  forall i h j h', rounds b i h j h' ->
-                   forall k h0,  rounds b k h0 i h ->
-                                 rounds b k h0 j h'. (* .no-out *)
+Lemma rounds_trans {B:Battle} :
+  forall i h j h', rounds B i h j h' ->
+                   forall k h0,  rounds B k h0 i h ->
+                                 rounds B k h0 j h'. (* .no-out *)
 (*| .. coq:: no-out |*)
 Proof. 
   intros i h j h' H k h0. induction 1 /dr. 
diff --git a/theories/ordinals/Hydra/Omega2_Small.v b/theories/ordinals/Hydra/Omega2_Small.v
index 87972e3e..8af74ed2 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.ON_wf (ON:=Omega2)) free m).
+    (Hvar: Hvariant (ON_Generic.ON_wf (ON:=Omega2)) free m).
 
   (* end snippet Impossibilitya *)
 
diff --git a/theories/ordinals/OrdinalNotations/ON_Finite.v b/theories/ordinals/OrdinalNotations/ON_Finite.v
index c969d12d..6147cd45 100644
--- a/theories/ordinals/OrdinalNotations/ON_Finite.v
+++ b/theories/ordinals/OrdinalNotations/ON_Finite.v
@@ -43,7 +43,7 @@ Abort.
 
 (* begin snippet compareDef:: no-out *)
 
-#[global] Instance compare_t {n:nat} : Compare (t n) :=
+#[global] Instance compare_fin {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) :
diff --git a/theories/ordinals/OrdinalNotations/ON_Generic.v b/theories/ordinals/OrdinalNotations/ON_Generic.v
index 4deb639b..a9b5a8c5 100644
--- a/theories/ordinals/OrdinalNotations/ON_Generic.v
+++ b/theories/ordinals/OrdinalNotations/ON_Generic.v
@@ -26,6 +26,7 @@ Class ON {A:Type} (lt: relation A) (cmp: Compare A) :=
   ON_comp :> Comparable lt cmp;
   ON_wf : well_founded lt;
   }.
+#[global] Existing Instance ON_comp.
 (* end snippet ONDef *)
 
 (* begin snippet ONDefsa:: no-out  *)
@@ -333,3 +334,5 @@ End SubON_properties.
 
 
 
+
+
diff --git a/theories/ordinals/OrdinalNotations/ON_O.v b/theories/ordinals/OrdinalNotations/ON_O.v
index eea86793..b7be307c 100644
--- a/theories/ordinals/OrdinalNotations/ON_O.v
+++ b/theories/ordinals/OrdinalNotations/ON_O.v
@@ -31,7 +31,7 @@ Definition le {a:A} : relation (t a) :=
   clos_refl (t a) lt.
 
 #[global]
-Instance compare_t {a:A} : Compare (t a) :=
+Instance compare_O {a:A} : Compare (t a) :=
 fun (alpha beta : t a) =>
   compare (proj1_sig alpha) (proj1_sig beta).
 
@@ -39,7 +39,7 @@ Lemma compare_correct {a} (alpha beta : t a) :
   CompSpec eq lt alpha beta (compare alpha beta).
 Proof.
  unfold CompSpec, compare.
-  - destruct alpha, beta; unfold compare,compare_t; cbn.
+  - destruct alpha, beta; unfold compare,compare_O; cbn.
     case_eq (compare x x0); unfold lt; cbn.
     + constructor 1.
       destruct (comparable_comp_spec x x0); try discriminate.
diff --git a/theories/ordinals/OrdinalNotations/ON_Omega2.v b/theories/ordinals/OrdinalNotations/ON_Omega2.v
index 087798e5..f85a6b6a 100644
--- a/theories/ordinals/OrdinalNotations/ON_Omega2.v
+++ b/theories/ordinals/OrdinalNotations/ON_Omega2.v
@@ -13,10 +13,10 @@ Open Scope ON_scope.
 
 (* begin snippet Omega2Def:: no-out *)
 
-#[ global ] Instance compare_nat_nat : Compare t :=
- compare_t compare_nat compare_nat.
+#[ global ] Instance compare_omega2 : Compare ON_mult.t :=
+ compare_mult compare_nat compare_nat.
 
-#[ global ] Instance Omega2: ON _ compare_nat_nat := ON_mult Omega Omega.
+#[ global ] Instance Omega2: ON _ compare_omega2 := ON_mult Omega Omega.
 
 Definition t := ON_t.
 (* end snippet Omega2Def *)
@@ -89,6 +89,7 @@ Qed.
 
 Lemma lt_succ_le alpha beta :
   alpha o< beta <-> succ alpha o<= beta. (* .no-out *)
+(* ... *)
 (*|
 .. coq:: none
 |*)
@@ -241,6 +242,7 @@ Qed.
 
 Lemma succ_ok alpha beta :
   Successor beta alpha <-> beta = succ alpha. (* .no-out *)
+(* ... *)
 (*|
 .. coq:: none 
 |*)
@@ -380,9 +382,8 @@ Infix "+" := plus : ON_scope.
 
 Lemma plus_compat (n p: nat) :
   fin  (n + p )%nat =  fin n + fin p. (* .no-out *)
-Proof. (* .no-out *)
-  destruct n; now cbn. 
-Qed.
+Proof. (* .no-out *) destruct n; reflexivity. Qed.
+
 (* end snippet plusDef *)
 
 
@@ -391,12 +392,10 @@ Qed.
 Compute 3 + omega.
 
 Compute omega + 3.
-(* end snippet plusExamples *)
-
-
-Example non_commutativity_of_plus :  omega + 3 <> 3 + omega. 
-Proof.  discriminate. Qed.
 
+Example non_commutativity_of_plus: omega + 3 <> 3 + omega. (* .no-out *)
+Proof.  (* .no-out *) discriminate. Qed.
+(* end snippet plusExamples *)
 
 (* begin snippet multFinDef *)
 
@@ -436,16 +435,14 @@ Proof. reflexivity. Qed.
 
 #[global] Instance plus_assoc: Assoc eq  plus. 
 Proof.
-  intros alpha beta gamma; destruct alpha, beta, gamma.
+  intros (n,n0) (n1, n2) (n3,n4); cbn. 
   destruct n,  n0, n1, n2, n3, n4; cbn; auto; f_equal; abstract lia.
 Qed.
 
-
 Lemma succ_is_plus_1  alpha : alpha + 1 = succ alpha.
 Proof.
- unfold succ ;
-simpl; 
- destruct alpha; cbn; destruct n, n0; try f_equal; abstract lia.
+ unfold succ ; cbn; destruct alpha; cbn; destruct n, n0; 
+   try f_equal; abstract lia.
 Qed.
 
 Lemma lt_omega alpha : alpha o< omega <-> exists n:nat,  alpha = fin n.
diff --git a/theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v b/theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v
index ef1acfcb..677a3565 100644
--- a/theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v
+++ b/theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v
@@ -15,15 +15,17 @@ Open Scope opo_scope.
 (* begin snippet OmegaPlusOmegaDef:: no-out *)
 
 #[global] Instance compare_nat_nat : Compare t :=
- compare_t compare_nat compare_nat.
+ compare_plus compare_nat compare_nat.
 
 #[global] Instance Omega_plus_Omega: ON _ compare_nat_nat :=
  ON_plus Omega Omega.
 
 Definition t := ON_t.
 
-Example ex1 : inl 7 o< inr 0. 
-Proof. now apply compare_lt_iff. Qed.
+Compute inl 42 o?= inr 0.
+
+Example ex1 : inl 7 o< inr 8. 
+Proof. apply compare_lt_iff. trivial. Qed.
 
 (* end snippet OmegaPlusOmegaDef *)
 
diff --git a/theories/ordinals/OrdinalNotations/ON_mult.v b/theories/ordinals/OrdinalNotations/ON_mult.v
index f048e137..3ac8b80f 100644
--- a/theories/ordinals/OrdinalNotations/ON_mult.v
+++ b/theories/ordinals/OrdinalNotations/ON_mult.v
@@ -35,7 +35,7 @@ Section Defs.
   Definition lt : relation t := lexico ltB ltA.
   Definition le := clos_refl _ lt. 
 
-  #[global] Instance compare_t : Compare t :=
+  #[global] Instance compare_mult : Compare t :=
     fun (alpha beta: t) =>
     match compare (fst alpha) (fst beta) with
     | Eq => compare (snd alpha) (snd beta)
@@ -66,7 +66,7 @@ Section Defs.
     | Gt => lt beta  alpha
     end.
   Proof.
-    destruct alpha, beta; cbn. unfold compare, compare_t; cbn.
+    destruct alpha, beta; cbn. unfold compare, compare_mult; cbn.
     destruct (comparable_comp_spec b b0).
     - subst; destruct (comparable_comp_spec a a0).
       + now subst.
@@ -86,25 +86,23 @@ Section Defs.
 
   (* begin snippet multComp:: no-out *)
 
-  #[global] Instance mult_comp:  Comparable lt compare_t.
-  (* end snippet multComp *)
-
-  Proof.
+  #[global] Instance mult_comp:  Comparable lt compare_mult.
+   Proof.
     split.
     - apply lt_strorder.
     - apply compare_correct.
   Qed. 
+  (* end snippet multComp *)
 
-  (* begin snippet ONMult:: no-out *)
-  #[global] Instance ON_mult: ON lt compare_t.
-  (* end snippet ONMult *)
 
-  Proof.
-    split.
+  (* begin snippet ONMult:: no-out *)
+  #[global] Instance ON_mult: ON lt compare_mult. 
+  Proof. 
+    split. 
     - apply mult_comp.
     - apply lt_wf.
   Qed.
-
+  (* end snippet ONMult *)
 
   Lemma lt_eq_lt_dec alpha beta :
     {lt alpha  beta} + {alpha = beta} + {lt beta alpha}.
diff --git a/theories/ordinals/OrdinalNotations/ON_plus.v b/theories/ordinals/OrdinalNotations/ON_plus.v
index f9b68d3b..3927bb97 100644
--- a/theories/ordinals/OrdinalNotations/ON_plus.v
+++ b/theories/ordinals/OrdinalNotations/ON_plus.v
@@ -23,14 +23,14 @@ Section Defs.
           (NB: ON ltB cmpB).
 
   Definition t := (A + B)%type.
-  Arguments inl  {A B} _.
-  Arguments inr  {A B} _.
+  Arguments inl {A B} _.
+  Arguments inr {A B} _.
 
   Definition lt : relation t := le_AsB _ _ ltA ltB.
 (* end snippet Defs *)
 
 (* begin snippet compareDef *)
-#[global] Instance compare_t : Compare t :=
+#[global] Instance compare_plus : Compare t :=
 fun (alpha beta: t) =>
    match alpha, beta with
      inl _, inr _ => Lt
@@ -53,21 +53,20 @@ Proof.
      subst.
      destruct (StrictOrder_Irreflexive _ H2).
   - intros x y z H H0.  inversion H; inversion H0; subst; try discriminate.
-    + injection H5;constructor.  subst.
-      now transitivity y0.    
+    + injection H5;constructor; subst; now transitivity y0.    
     + constructor.
     + constructor.
     + constructor.
-      injection H5; intro; subst.  now transitivity y0.
+      injection H5; intro; subst; now transitivity y0.
 Qed.
     
 
 Lemma compare_reflect alpha beta :
   match (compare alpha beta)
   with
-    Lt => lt alpha  beta
+    Lt => lt alpha beta
   | Eq => alpha = beta
-  | Gt => lt beta  alpha
+  | Gt => lt beta alpha
   end.
   destruct alpha, beta; cbn; auto.
   destruct (comparable_comp_spec a a0); (now subst || constructor; auto).
@@ -88,7 +87,7 @@ Qed.
 
 (* begin snippet plusComp:: no-out *)
 
-#[global] Instance plus_comp : Comparable lt compare_t.
+#[global] Instance plus_comp : Comparable lt compare_plus.
 Proof.  split; [apply lt_strorder | apply compare_correct]. Qed.
 (* end snippet plusComp *)
 
@@ -115,7 +114,7 @@ Qed.
 .. coq:: no-out 
 |*)
 
-#[global] Instance ON_plus : ON lt compare_t.
+#[global] Instance ON_plus : ON lt compare_plus.
 Proof. split; [apply plus_comp | apply lt_wf]. Qed.
 
 (*||*)
diff --git a/theories/ordinals/OrdinalNotations/OmegaOmega.v b/theories/ordinals/OrdinalNotations/OmegaOmega.v
index 799f8f8b..96379730 100644
--- a/theories/ordinals/OrdinalNotations/OmegaOmega.v
+++ b/theories/ordinals/OrdinalNotations/OmegaOmega.v
@@ -86,7 +86,7 @@ Module LO.
   Qed.
 
   (* begin snippet compareDef:: no-out  *)
-  #[ global ] Instance compare_t : Compare t :=
+  #[ global ] Instance compare_oo : Compare t :=
   fix cmp (a b : t) :=
     match a, b with
     | nil, nil => Eq
@@ -500,7 +500,7 @@ Module OO.
   Definition lt (alpha beta: OO) := LO.lt (data alpha) (data beta).
   Definition le := leq lt.
   #[ global ] Instance compare_OO : Compare OO := 
-    fun (alpha beta: OO) => LO.compare_t (data alpha) (data beta).
+    fun (alpha beta: OO) => LO.compare_oo (data alpha) (data beta).
   (*  end snippet OODef *)
 
   #[ global ] Instance Zero : OO := @mkord nil refl_equal.
@@ -598,7 +598,8 @@ Module OO.
     - destruct a, b; cbn.
       destruct (comparable_comp_spec data0 data1).
       + subst.
-        assert (compare_t data1 data1 = compare data1 data1) by reflexivity.
+        assert (compare_oo data1 data1 = compare data1 data1) 
+          by reflexivity.
         rewrite H.
         rewrite compare_refl.
         constructor.