diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 2685a80e..fb5ad432 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -16,6 +16,7 @@ jobs:
       matrix:
         image:
           - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
           - 'mathcomp/mathcomp:1.13.0-coq-8.14'
           - 'mathcomp/mathcomp:1.13.0-coq-8.13'
           - 'mathcomp/mathcomp:1.12.0-coq-8.14'
diff --git a/.nix/coq-overlays/hydra-battles-single/default.nix b/.nix/coq-overlays/hydra-battles-single/default.nix
index f870b464..ffeba89a 100644
--- a/.nix/coq-overlays/hydra-battles-single/default.nix
+++ b/.nix/coq-overlays/hydra-battles-single/default.nix
@@ -1,5 +1,5 @@
 { lib, mkCoqDerivation, coq, version ? null
-, equations, gaia, mathcomp-ssreflect, mathcomp-algebra, mathcomp-zify, paramcoq
+, equations, gaia, LibHyps, mathcomp-ssreflect, mathcomp-algebra, mathcomp-zify, paramcoq
 , python3Packages, serapi, texlive, withMovies ? true, withTex ? true }:
 
 with lib; mkCoqDerivation rec {
@@ -45,6 +45,7 @@ with lib; mkCoqDerivation rec {
   propagatedBuildInputs = [
     equations
     gaia
+    LibHyps
     mathcomp-ssreflect
     mathcomp-algebra
     mathcomp-zify
diff --git a/.nix/coq-overlays/hydra-battles/default.nix b/.nix/coq-overlays/hydra-battles/default.nix
new file mode 100644
index 00000000..2309bb6a
--- /dev/null
+++ b/.nix/coq-overlays/hydra-battles/default.nix
@@ -0,0 +1,35 @@
+{ lib, mkCoqDerivation, coq, equations, LibHyps, version ? null }:
+with lib;
+
+mkCoqDerivation {
+  pname = "hydra-battles";
+  owner = "coq-community";
+
+  release."0.4".sha256 = "1f7pc4w3kir4c9p0fjx5l77401bx12y72nmqxrqs3qqd3iynvqlp";
+  release."0.5".sha256 = "121pcbn6v59l0c165ha9n00whbddpy11npx2y9cn7g879sfk2nqk";
+  releaseRev = (v: "v${v}");
+
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = range "8.13" "8.14"; out = "0.5"; }
+    { case = range "8.11" "8.12"; out = "0.4"; }
+  ] null;
+
+  propagatedBuildInputs = [ equations LibHyps ];
+
+  useDune2 = true;
+
+  meta = {
+    description = "Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq";
+    longDescription = ''
+      An exploration of some properties of Kirby and Paris' hydra
+      battles, with the help of the Coq Proof assistant. This
+      development includes the study of several representations of
+      ordinal numbers, and a part of the so-called Ketonen and Solovay
+      machinery (combinatorial properties of epsilon0).
+    '';
+    maintainers = with maintainers; [ siraben Zimmi48 ];
+    license = licenses.mit;
+    platforms = platforms.unix;
+  };
+}
diff --git a/.nix/nixpkgs.nix b/.nix/nixpkgs.nix
new file mode 100644
index 00000000..9efb526f
--- /dev/null
+++ b/.nix/nixpkgs.nix
@@ -0,0 +1,4 @@
+fetchTarball {
+         url = https://github.com/Zimmi48/nixpkgs/archive/c9c002d30a165fe0ecfec348de66bbe910ac1a57.tar.gz;
+         sha256 = "05mx4mmw0px0sylal287clpj3s6gm2qy0djjaxxm71s06y2j5fv6";
+       }
diff --git a/README.md b/README.md
index fe1140ad..54a26e34 100644
--- a/README.md
+++ b/README.md
@@ -65,6 +65,7 @@ in the proceedings of [JFLA 2022](http://jfla.inria.fr/jfla2022.html).
   - [MathComp Algebra](https://github.com/math-comp/math-comp)
   - [Gaia](https://github.com/coq-community/gaia) 1.12 or later
   - [Mczify](https://github.com/math-comp/mczify)
+  - [LibHyps](https://github.com/Matafou/LibHyps)
 - Coq namespaces: `hydras`, `additions`, `gaia_hydras`
 - Related publication(s):
   - [Hydras & Co.: Formalized mathematics in Coq for inspiration and entertainment](https://hal.archives-ouvertes.fr/hal-03404668) 
diff --git a/_CoqProject b/_CoqProject
index 662bd523..0925a66c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -171,4 +171,10 @@ theories/gaia/T1Bridge.v
 theories/gaia/GaiaToHydra.v
 theories/gaia/nfwfgaia.v
 theories/gaia/GCanon.v
+
+
+theories/ordinals/Prelude/MoreLibHyps.v
+theories/ordinals/Prelude/LibHyps_Experiments.v
+
 theories/gaia/GF_alpha.v
+
diff --git a/coq-addition-chains.opam b/coq-addition-chains.opam
index c41cae7b..dfb30949 100644
--- a/coq-addition-chains.opam
+++ b/coq-addition-chains.opam
@@ -17,9 +17,9 @@ correctness."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
-  "coq" {(>= "8.13" & < "8.15~") | (= "dev")}
+  "coq" {(>= "8.13" & < "8.16~") | (= "dev")}
   "coq-paramcoq" {(>= "1.1.3" & < "1.2~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.12.0" & < "1.14~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "1.12.0" & < "1.15~") | (= "dev")}
   "coq-mathcomp-algebra"
 ]
 
diff --git a/coq-gaia-hydras.opam b/coq-gaia-hydras.opam
index db296486..2f4cd8ad 100644
--- a/coq-gaia-hydras.opam
+++ b/coq-gaia-hydras.opam
@@ -16,11 +16,11 @@ similar concepts in the two projects."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
-  "coq" {(>= "8.13" & < "8.15~") | (= "dev")}
+  "coq" {(>= "8.13" & < "8.16~") | (= "dev")}
   "coq-hydra-battles" {= version}
-  "coq-mathcomp-ssreflect" {(>= "1.12.0" & < "1.14~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "1.12.0" & < "1.15~") | (= "dev")}
   "coq-mathcomp-zify"
-  "coq-gaia" {(>= "1.12" & < "1.14~") | (= "dev")}
+  "coq-gaia" {(>= "1.12" & < "1.15~") | (= "dev")}
 ]
 
 tags: [
diff --git a/coq-hydra-battles.opam b/coq-hydra-battles.opam
index 577fa48c..9f7ba7de 100644
--- a/coq-hydra-battles.opam
+++ b/coq-hydra-battles.opam
@@ -18,8 +18,9 @@ properties of epsilon0)."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
-  "coq" {(>= "8.13" & < "8.15~") | (= "dev")}
+  "coq" {(>= "8.13" & < "8.16~") | (= "dev")}
   "coq-equations" {(>= "1.2" & < "1.4~") | (= "dev")}
+  "coq-libhyps"
 ]
 
 tags: [
diff --git a/meta.yml b/meta.yml
index 09d153a2..ff99f4dc 100644
--- a/meta.yml
+++ b/meta.yml
@@ -104,11 +104,13 @@ license:
 
 supported_coq_versions:
   text: 8.13 or later
-  opam: '{(>= "8.13" & < "8.15~") | (= "dev")}'
+  opam: '{(>= "8.13" & < "8.16~") | (= "dev")}'
 
 tested_coq_opam_versions:
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'
+- version: '1.14.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.14'
   repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.13'
@@ -131,7 +133,7 @@ dependencies:
     [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "1.12.0" & < "1.14~") | (= "dev")}'
+    version: '{(>= "1.12.0" & < "1.15~") | (= "dev")}'
   description: |-
     [MathComp SSReflect](https://github.com/math-comp/math-comp) 1.12 or later
 - opam:
@@ -140,13 +142,17 @@ dependencies:
     [MathComp Algebra](https://github.com/math-comp/math-comp)
 - opam:
     name: coq-gaia
-    version: '{(>= "1.12" & < "1.14~") | (= "dev")}'
+    version: '{(>= "1.12" & < "1.15~") | (= "dev")}'
   description: |-
     [Gaia](https://github.com/coq-community/gaia) 1.12 or later
 - opam:
     name: coq-mathcomp-zify
   description: |-
     [Mczify](https://github.com/math-comp/mczify)
+- opam:
+    name: coq-libhyps
+  description: |-
+    [LibHyps](https://github.com/Matafou/LibHyps)
 
 namespace: hydras
 
diff --git a/theories/gaia/T1Bridge.v b/theories/gaia/T1Bridge.v
index 34404ebf..20a164cc 100644
--- a/theories/gaia/T1Bridge.v
+++ b/theories/gaia/T1Bridge.v
@@ -115,7 +115,7 @@ Qed.
 Lemma h2g_eq_iff (a b :hT1) :  h2g a = h2g b <-> a = b.
 (* end snippet h2gEqIff *)
 Proof. 
-    split.
+  split.
     -  rewrite  -(g2h_h2gK a) -(g2h_h2gK b) !h2g_g2hK  =>  // -> //.
     - move => -> //. 
 Qed.
@@ -149,7 +149,6 @@ Proof.
   by rewrite Href g2h_h2gK.
 Qed.
 
-
 Lemma refines2_R f f' :
   refines2 f f' ->
   forall y z: T1, f (g2h y) (g2h z) = g2h (f' y z).
@@ -160,6 +159,7 @@ Qed.
 
 (** Refinements of usual constants *)
 (* begin snippet constantRefs:: no-out *)
+
 Lemma zero_ref : refines0 hzero zero.
 Proof. by []. Qed.
 
@@ -456,9 +456,8 @@ Lemma nf_ref (a: hT1)  : hnfb a = T1nf (h2g a).
 (* end snippet nfRef *)
 Proof.
   elim: a => //.
-  - move => a IHa n b IHb; rewrite Epsilon0.T1.nf_b_cons_eq; simpl T1nf. 
-    rewrite IHa IHb;  change (phi0 (h2g a)) with (h2g (Epsilon0.T1.phi0 a)).
-    by rewrite andbA decide_hlt_rw.
+  - move => a IHa n b IHb; rewrite T1.nf_b_cons_eq; simpl T1nf. 
+    by rewrite IHa IHb [phi0 (h2g a)]/(h2g (T1.phi0 a)) andbA decide_hlt_rw.
 Qed.
 
 Lemma LT_ref : refinesRel  hLT  gLT.
@@ -468,39 +467,30 @@ Proof.
     + by rewrite  -nf_ref.
     + by apply lt_ref. 
     + by rewrite -nf_ref. 
-  -  case => H H0 H1; repeat  split. 
-     +  red; by rewrite nf_ref.
-     + by apply lt_ref. 
-     +  red; by rewrite nf_ref.
+  -  case => H H0 H1; repeat  split; red; rewrite ?nf_ref ?lt_ref => // ;
+            by apply lt_ref. 
 Qed. 
 
 
 Lemma LE_ref : refinesRel hLE gLE.
 Proof. 
   split. 
-  - case => a b.
-    split. 
-    rewrite -nf_ref => //.
-    case: b => c _.    
-    destruct c. 
-    
-    apply T1ltW. 
-    rewrite - decide_hlt_rw => //.
-    red;  rewrite bool_decide_eq_true => //.
-    apply T1lenn. 
-    case b => _ H.
-    rewrite - nf_ref => //. 
-  - case.
-    rewrite /hLE; split. 
-    rewrite -nf_ref in p p1 => //.
-    split => //.
-    rewrite T1le_eqVlt in p0. move : p0 => /orP.
-    case => /eqP Heq; subst.  rewrite h2g_eq_iff in Heq; subst. 
-    right. 
-    left. 
-    rewrite -decide_hlt_rw in Heq => //.
-    move: Heq => /eqP H. rewrite bool_decide_eq_true in H => //.
-    rewrite -nf_ref in p1 => //.
+  - case => a b; split. 
+    + rewrite -nf_ref => //.
+    + case: b => c _; case :c => [y0 Hy0 |].
+      apply T1ltW. 
+      * rewrite - decide_hlt_rw => //.
+        red;  rewrite bool_decide_eq_true => //.
+      *  apply T1lenn. 
+    +  case b => _ ?; rewrite - nf_ref => //. 
+  - case; rewrite /hLE; repeat split => //.
+   +  rewrite -nf_ref in p p1 => //.
+   +  rewrite T1le_eqVlt in p0; move : p0 => /orP.
+      case => /eqP Heq; subst.
+      * rewrite h2g_eq_iff in Heq; subst; right. 
+      *    left; rewrite -decide_hlt_rw in Heq => //.
+           move: Heq => /eqP H;  rewrite bool_decide_eq_true in H => //.
+   + rewrite -nf_ref in p1 => //.
 Qed.
 
 
diff --git a/theories/ordinals/Prelude/Iterates.v b/theories/ordinals/Prelude/Iterates.v
index 2ef658a4..fd268bd1 100644
--- a/theories/ordinals/Prelude/Iterates.v
+++ b/theories/ordinals/Prelude/Iterates.v
@@ -1,6 +1,8 @@
 (**  Iteration of a function (similar to [Nat.iter]) 
      Abstract Properties
 
+Experimental use of LibHyps 
+
 *)
 
 
@@ -8,6 +10,9 @@ Open Scope nat_scope.
 From Coq Require Import RelationClasses Relations Arith Max Lia.
 From hydras Require Import Exp2.
 
+From hydras Require Import MoreLibHyps.
+Ltac rename_hyp n th ::= rename_short n th.
+
 (* begin snippet iterateDef *)
 
 Fixpoint iterate {A:Type}(f : A -> A) (n: nat)(x:A) :=
@@ -151,9 +156,6 @@ Proof.
     eapply dominates_from_trans with g; eauto.
 Qed.
 
-
-
-
 (** ** Abstract properties of iterate *)
 
 
@@ -164,7 +166,7 @@ Proof. reflexivity. Qed.
 Lemma iterate_S_eqn2 {A:Type}(f : A -> A) (n: nat)(x:A):
   iterate f (S n) x =  (iterate f n (f x)).
 Proof.
-  induction n. 
+  induction n.
   - reflexivity.
   - rewrite (iterate_S_eqn f (S n)), IHn;  reflexivity. 
 Qed.
@@ -215,23 +217,20 @@ Lemma iterate_lt_from f k:
                        forall z : nat, k <= z ->
                                        iterate f i z < iterate f j z.
 Proof.
-  induction 3.
- - intros; rewrite iterate_S_eqn; auto.
-   apply H0.
-   revert i; induction i.
+  induction 3 /r.
+ - intros Hmono Hind * Hkz; rewrite iterate_S_eqn; auto.
+   apply Hind;  revert i; induction i /r. 
    +  cbn; auto. 
    +  transitivity (iterate f i z); auto.
-      rewrite iterate_S_eqn.
-      apply Lt.lt_le_weak.
-      apply H0; auto. 
- - intros; transitivity (iterate f m z); auto. 
-   rewrite iterate_S_eqn; apply H0.
+      rewrite iterate_S_eqn; apply Lt.lt_le_weak.
+      apply Hind; auto. 
+ - intros Hmono Hind * Hlt Hind2 * Kkz; transitivity (iterate f m z); auto. 
+   rewrite iterate_S_eqn; apply Hind. 
    transitivity z; auto.
-   clear i H1 IHle; induction m.
+   clear i Hlt Hind2; induction m.
    + cbn; auto.
-   + cbn; transitivity (iterate f m z); auto.
-     apply Lt.lt_le_weak, H0.
-     lia.
+      + cbn; transitivity (iterate f m z); auto.
+     apply Lt.lt_le_weak, Hind;  lia. 
 Qed. 
 
 
@@ -244,9 +243,9 @@ Lemma iterate_le_n_Sn (f: nat -> nat):
 (* end snippet iterateLeNSN *)
 
 Proof.
-  induction n.
+  induction n /n.
   - cbn; auto with arith.
-  - cbn; intros; apply H.
+  - cbn; intros; apply  h_all_le_x_. 
 Qed.
 
 Lemma iterate_le_np_le (f: nat -> nat):
@@ -298,36 +297,37 @@ Qed.
 Lemma iterate_ge' : forall f,  id <<= f ->
                                forall n j, 0 < n -> j <= iterate f n j.
 Proof.
-  induction n.
-  - inversion 1.
-  - intros j H0; destruct n.
-    + simpl; apply H.
-    +  transitivity (iterate f (S n) j).
-       * apply IHn; auto with arith.
-       * simpl; apply H.
+  induction n /r. 
+  - inversion 2.
+  - intros *  H0; destruct n /r. 
+    + simpl; intros /n. apply h_fun_le_id_.
+    +  intros /n;  transitivity (iterate f (S n) j).
+       * auto with arith.
+       * simpl; apply h_fun_le_id_.
 Qed.
 
+
 Lemma iterate_ge'' f : id <<= f -> strict_mono f -> forall i k,
       k <= Nat.pred (iterate (fun z => S (f z)) (S i) k).
 Proof.
-  induction i.
-  - intros; cbn; apply H.
-  - intros;  rewrite iterate_rw;
+  induction i /n.
+  - intros; cbn; apply h_fun_le_id_.
+  - intros *;   rewrite iterate_rw;
     apply le_trans with
         (Nat.pred (iterate (fun z : nat => S (f z)) (S i) k)).
     + auto.
     + cbn;  assert (H1: strict_mono (fun z => S (f z))).
-      { intros x y Hlt; apply H0 in Hlt;  auto with arith. }
+      { intros x y Hlt.  apply h_strict_mono_ in Hlt;  auto with arith. }
       generalize  (iterate_mono _ H1).
       assert (H2: S <<= (fun z : nat => S (f z))).
       { intro x; auto with arith.
-        specialize (H x); auto with arith.
+        specialize (h_fun_le_id_ x); auto with arith.
       }
       intros H3;  specialize (H3 H2 i).
       apply Nat.lt_le_incl.
       assert (H4: k < S (f k)).
       { apply le_lt_trans with (f k).
-        - apply H.                       
+        - apply h_fun_le_id_.                       
         - auto with arith.
       }
    specialize (H3 _ _ H4); auto.
@@ -395,7 +395,7 @@ Proof.
   - intro H0; inversion H0.
   - destruct k.
     + simpl;  intros _ l Hl;  apply H; auto.
-    + intros _ l Hl; repeat rewrite iterate_S_eqn.
+    + intros _ l Hl; {autorename}.  repeat rewrite iterate_S_eqn.
       transitivity (g (f (iterate f k l))).
       * apply H; transitivity (f l).
         { transitivity l;  auto. 
diff --git a/theories/ordinals/Prelude/LibHyps_Experiments.v b/theories/ordinals/Prelude/LibHyps_Experiments.v
new file mode 100644
index 00000000..a10afb48
--- /dev/null
+++ b/theories/ordinals/Prelude/LibHyps_Experiments.v
@@ -0,0 +1,32 @@
+From LibHyps Require Export LibHyps.
+Require Export MoreLibHyps. 
+
+(*  move to experimental file (not to export *)
+
+Require Import List.
+Import ListNotations. 
+Local Open Scope autonaming_scope.
+
+Ltac rename_hyp n th ::= rename_short n th.
+
+Goal forall n p , n <= p -> forall q, p <= q -> n <= q.
+induction 1  /n.
+- intros; assumption.
+- intros /n.  apply h_all_le_n_; transitivity (S m); auto.
+Qed.
+
+Goal forall n p , n <= p -> forall q, p <= q -> n <= q.
+  intros * H; elim H.
+  - intros /n.  assumption.
+  - intros /n.  apply h_all_le_n_; transitivity (S m); auto.
+Qed.
+
+Require Import Arith. 
+Parameters f g h : nat -> nat.
+Parameter P : nat->nat->nat-> Prop.
+Goal forall x y ,  f (g (h x)) = h (g (f y)) -> x = y -> x < y ->
+                   P  x y x  -> f y <> f x.
+  intros x y H H0 H1 H2 /n. subst y.
+  absurd (x < x) ; trivial. 
+  apply Nat.lt_irrefl. 
+Qed. 
diff --git a/theories/ordinals/Prelude/MoreLibHyps.v b/theories/ordinals/Prelude/MoreLibHyps.v
new file mode 100644
index 00000000..7027aa52
--- /dev/null
+++ b/theories/ordinals/Prelude/MoreLibHyps.v
@@ -0,0 +1,24 @@
+From LibHyps Require Export LibHyps.
+
+Require Import List.
+Import ListNotations. 
+#[local] Open Scope autonaming_scope.
+
+
+Tactic Notation (at level 4) tactic4(Tac) "/" "dr" := Tac ; {< fun h
+=> try revert dependent h }.
+Tactic Notation (at level 4) tactic4(Tac) "/" "r?" :=
+  Tac ; {< fun h  => try revert h }.
+
+
+(*  move to experimental file (not to export *)
+
+
+Ltac old_rename := rename_hyp_default.
+
+Ltac rename_short n th :=
+  match th with
+  | (?f ?x ?y) => name ((f # 1) ++ (x # 1))                          
+  | (?f ?x) => name ((f # 1))
+  | _ => old_rename n th
+  end.