From 6b570f626138495d7a738383779b2b9be5392c76 Mon Sep 17 00:00:00 2001
From: Timur Aminev <ablearthy@gmail.com>
Date: Wed, 1 Jan 2025 17:19:02 +0300
Subject: [PATCH 01/15] Update prelude and sorting

---
 _CoqProject   | 32 ++++++++++++++++----------------
 src/prelude.v | 10 +++++-----
 src/sorting.v | 14 +++++++-------
 3 files changed, 28 insertions(+), 28 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 6ba87fa..0a4f71d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5,19 +5,19 @@
 src/prelude.v
 src/basics.v
 src/sorting.v
-src/selection.v
-src/bintree.v
-src/bst.v
-src/adt.v
-src/twothree.v
-src/redblack.v
-src/avl.v
-src/beyond.v
-src/braun.v
-src/trie.v
-src/quadtree.v
-src/priority.v
-src/leftist.v
-src/braun_queue.v
-src/binom_heap.v
-src/huffman.v
\ No newline at end of file
+# src/selection.v
+# src/bintree.v
+# src/bst.v
+# src/adt.v
+# src/twothree.v
+# src/redblack.v
+# src/avl.v
+# src/beyond.v
+# src/braun.v
+# src/trie.v
+# src/quadtree.v
+# src/priority.v
+# src/leftist.v
+# src/braun_queue.v
+# src/binom_heap.v
+# src/huffman.v
\ No newline at end of file
diff --git a/src/prelude.v b/src/prelude.v
index c0f6722..e031487 100644
--- a/src/prelude.v
+++ b/src/prelude.v
@@ -337,7 +337,7 @@ Proof. by case: xs=>//=x s; rewrite size_belast. Qed.
 End Butlast.
 
 Section Mins.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 Variable (x0 : T).
 
 Import Order.POrderTheory.
@@ -351,7 +351,7 @@ Proof.
 case: xs=>//=x xs _; elim/last_ind: xs=>/=.
 - by rewrite lexx inE eq_refl.
 move=>xs y /andP [/andP [IH1 IH2]]; rewrite !inE=>IH3.
-rewrite foldl_rcons le_minl IH1 /= mem_rcons inE eq_minr all_rcons le_minl lexx orbT /=.
+rewrite foldl_rcons ge_min IH1 /= mem_rcons inE eq_minr all_rcons ge_min lexx orbT /=.
 rewrite {1 3 6}/Order.min; case: ifP.
 - by rewrite IH2 /= =>H; case/orP: IH3=>[/eqP->|->]; rewrite ?eqxx ?orbT.
 move/negbT; rewrite -leNgt=>Hy; rewrite Hy /= orbT andbT.
@@ -366,7 +366,7 @@ Lemma all_foldl_le (x : T) xs y :
 Proof.
 move=>Hyx; elim/last_ind: xs=>//=t h IH.
 rewrite all_rcons foldl_rcons; case/andP=>Hy Ha.
-by rewrite le_minr Hy IH.
+by rewrite le_min Hy IH.
 Qed.
 
 Lemma all_foldl_eq (x : T) xs :
@@ -426,8 +426,8 @@ case/andP: (mins_min_in Hx)=>Hax Hix.
 case/andP: (mins_min_in Hy)=>Hay Hiy.
 apply/andP; split.
 - rewrite all_cat; apply/andP; split.
-  - by apply/sub_all/Hax=>z Hz; rewrite le_minl Hz.
-  by apply/sub_all/Hay=>z Hz; rewrite le_minl Hz orbT.
+  - by apply/sub_all/Hax=>z Hz; rewrite ge_min Hz.
+  by apply/sub_all/Hay=>z Hz; rewrite ge_min Hz orbT.
 rewrite minElt; case: ifP=>_; rewrite mem_cat.
 - by rewrite Hix.
 by rewrite Hiy orbT.
diff --git a/src/sorting.v b/src/sorting.v
index d47b8ed..7518b36 100644
--- a/src/sorting.v
+++ b/src/sorting.v
@@ -11,7 +11,7 @@ Import Order.TotalTheory.
 Open Scope order_scope.
 
 Section InsertionSort.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 Implicit Types (xs ys : seq T).
 
 (* Definition *)
@@ -111,7 +111,7 @@ Admitted.
 End InsertionSortNat.
 
 Section QuickSort.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 Implicit Types (xs ys : seq T).
 
 (* Definition *)
@@ -221,7 +221,7 @@ Admitted.
 End QuickSort.
 
 Section TopDownMergeSort.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 Implicit Types (xs ys : seq T).
 
 (* reusing `merge` from mathcomp.path *)
@@ -332,7 +332,7 @@ Admitted.
 End TopDownMergeSort.
 
 Section BottomUpMergeSort.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 Implicit Types (xs ys : seq T).
 
 Equations merge_adj : seq (seq T) -> seq (seq T) :=
@@ -459,7 +459,7 @@ Qed.
 End BottomUpMergeSort.
 
 Section NaturalMergeSort.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 Implicit Types (xs ys : seq T) (xss : seq (seq T)).
 
 Fixpoint runs_fix a xs : seq (seq T) :=
@@ -699,7 +699,7 @@ Qed.
 End NaturalMergeSort.
 
 Section UniquenessOfSorting.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 Implicit Types (xs ys : seq T).
 
 (* this already exists in path.v as sorted_eq *)
@@ -738,7 +738,7 @@ Qed.
 End UniquenessOfSorting.
 
 Section Stability.
-Context {disp : unit} {T : eqType} {K : orderType disp}.
+Context {disp : Order.disp_t} {T : eqType} {K : orderType disp}.
 Implicit Types (xs ys : seq T).
 
 (* Definition *)

From 9a35cd8b779bc3a10fdfd24efa9f3247eadbe109 Mon Sep 17 00:00:00 2001
From: Timur Aminev <ablearthy@gmail.com>
Date: Sun, 5 Jan 2025 04:13:42 +0300
Subject: [PATCH 02/15] Update selection

---
 _CoqProject     |  2 +-
 src/selection.v | 10 +++++-----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 0a4f71d..62c1bba 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5,7 +5,7 @@
 src/prelude.v
 src/basics.v
 src/sorting.v
-# src/selection.v
+src/selection.v
 # src/bintree.v
 # src/bst.v
 # src/adt.v
diff --git a/src/selection.v b/src/selection.v
index 685aae6..19d6946 100644
--- a/src/selection.v
+++ b/src/selection.v
@@ -11,7 +11,7 @@ Import Order.TotalTheory.
 Open Scope order_scope.
 
 Section Intro.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 Implicit Types (xs ys : seq T) (k : nat).
 Variable x0 : T.
 
@@ -154,7 +154,7 @@ End IntroInt.
 
 Section DivideAndConquer.
 
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 Implicit Types (xs ys zs : seq T) (k : nat).
 Variable x0 : T.
 
@@ -225,7 +225,7 @@ End DivideAndConquer.
 
 Section MedianOfMedians.
 
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 Implicit Types (xs ys zs : seq T) (k : nat).
 Variable x0 : T.
 
@@ -485,7 +485,7 @@ Qed.
 End MedianOfMedians.
 
 Section SelectionInLinearTime.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 Implicit Types (xs ys zs : seq T) (k : nat).
 Variable x0 : T.
 
@@ -600,7 +600,7 @@ Proof. by rewrite mom_select_correct; apply: is_selection_select. Qed.
 End SelectionInLinearTime.
 
 Section TimeFunctions.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 Implicit Types (xs ys zs : seq T) (k : nat).
 Variable x0 : T.
 

From 2ac973d61b2a703207308d3ab109c03787cb4f70 Mon Sep 17 00:00:00 2001
From: Timur Aminev <ablearthy@gmail.com>
Date: Sun, 5 Jan 2025 04:26:13 +0300
Subject: [PATCH 03/15] Update bintree

---
 _CoqProject   |  2 +-
 src/bintree.v | 11 +++++++----
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 62c1bba..166b37f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6,7 +6,7 @@ src/prelude.v
 src/basics.v
 src/sorting.v
 src/selection.v
-# src/bintree.v
+src/bintree.v
 # src/bst.v
 # src/adt.v
 # src/twothree.v
diff --git a/src/bintree.v b/src/bintree.v
index 7e74b47..1f4428b 100644
--- a/src/bintree.v
+++ b/src/bintree.v
@@ -1,5 +1,6 @@
 From Equations Require Import Equations.
 From Coq Require Import ssreflect ssrbool ssrfun.
+From HB Require Import structures.
 From mathcomp Require Import eqtype ssrnat seq prime.
 From favssr Require Import prelude.
 Set Implicit Arguments.
@@ -157,8 +158,10 @@ apply: (iffP andP).
 by case=><-<-; split; [apply/IHl|apply/IHr].
 Qed.
 
-Canonical tree_eqMixin := EqMixin eqtreeP.
-Canonical tree_eqType := Eval hnf in EqType (tree T) tree_eqMixin.
+HB.instance Definition _ := hasDecEq.Build (tree T) eqtreeP.
+
+(* Canonical tree_eqMixin := EqMixin eqtreeP.
+Canonical tree_eqType := Eval hnf in EqType (tree T) tree_eqMixin. *)
 
 Lemma perm_pre_in (t : tree T) : perm_eq (inorder t) (preorder t).
 Proof.
@@ -609,13 +612,13 @@ Admitted.
 
 (* Exercise 4.6 *)
 
-Context {disp : unit} {P : orderType disp}.
+Context {disp : Order.disp_t} {P : orderType disp}.
 Variable (x0 : P) (lmin : left_id x0 Order.max).
 
 Lemma rmin : right_id x0 Order.max.
 Proof. by move=>x; rewrite maxC lmin. Qed.
 
-Canonical max_monoid := Monoid.Law maxA lmin rmin.
+HB.instance Definition _ := Monoid.isLaw.Build P x0 Order.max maxA lmin rmin.
 
 Definition max_seq (xs : seq P) : P :=
   \big[Order.max/x0]_(x<-xs) x.

From 8ce46d20400f6d5b70188bcbf69c83a61a6471c0 Mon Sep 17 00:00:00 2001
From: Timur Aminev <ablearthy@gmail.com>
Date: Sun, 5 Jan 2025 05:07:59 +0300
Subject: [PATCH 04/15] Update bst

---
 _CoqProject |  2 +-
 src/bst.v   | 47 ++++++++++++++++++-----------------------------
 2 files changed, 19 insertions(+), 30 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 166b37f..a11176c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -7,7 +7,7 @@ src/basics.v
 src/sorting.v
 src/selection.v
 src/bintree.v
-# src/bst.v
+src/bst.v
 # src/adt.v
 # src/twothree.v
 # src/redblack.v
diff --git a/src/bst.v b/src/bst.v
index 9e03cc1..5228355 100644
--- a/src/bst.v
+++ b/src/bst.v
@@ -1,5 +1,6 @@
 From Equations Require Import Equations.
 From Coq Require Import ssreflect ssrbool ssrfun.
+From HB Require Import structures.
 From mathcomp Require Import eqtype choice ssrnat seq order path.
 From favssr Require Import prelude bintree.
 Set Implicit Arguments.
@@ -11,7 +12,7 @@ Import Order.TotalTheory.
 Open Scope order_scope.
 
 Section Intro.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Fixpoint bst (t : tree T) : bool :=
   if t is Node l a r
@@ -51,7 +52,7 @@ Admitted.
 End Intro.
 
 Module ASet.
-Structure ASet (disp : unit) (T : orderType disp): Type :=
+Structure ASet (disp : Order.disp_t) (T : orderType disp): Type :=
   make {tp :> Type;
         empty : tp;
         insert : T -> tp -> tp;
@@ -61,7 +62,7 @@ Structure ASet (disp : unit) (T : orderType disp): Type :=
 End ASet.
 
 Section Unbalanced.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Variant cmp_val := LT | EQ | GT.
 
@@ -179,7 +180,7 @@ Admitted.
 End Unbalanced.
 
 Section Correctness.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 (* Exercise 5.3 *)
 
@@ -238,7 +239,7 @@ Admitted.
 End Correctness.
 
 Section CorrectnessProofs.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 (* sorted list library *)
 
@@ -459,7 +460,7 @@ Definition LASet := ASet.make [::] ins_list del_list (@mem_seq T).
 End CorrectnessProofs.
 
 Section TreeRotations.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Fixpoint is_list (t : tree T) : bool :=
   if t is Node l _ r then ~~ is_node l && is_list r else true.
@@ -630,7 +631,7 @@ Proof.
 Admitted.
 
 Section Augmented.
-Context {disp : unit} {T : orderType disp} {A : Type}.
+Context {disp : Order.disp_t} {T : orderType disp} {A : Type}.
 Implicit Types (t : tree (T*A)).
 
 Fixpoint isin_a t x : bool :=
@@ -690,18 +691,15 @@ Qed.
 End Augmented.
 
 Section IntervalTrees.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 (* intervals *)
 
 Structure ivl : Type := Interval {ival :> T * T; _ : ival.1 <= ival.2}.
 
-Canonical interval_subType := Eval hnf in [subType for ival].
-
-Definition interval_eqMixin := Eval hnf in [eqMixin of ivl by <:].
-Canonical interval_eqType := Eval hnf in EqType ivl interval_eqMixin.
-Definition interval_choiceMixin := [choiceMixin of ivl by <:].
-Canonical interval_choiceType := Eval hnf in ChoiceType ivl interval_choiceMixin.
+HB.instance Definition _ := [isSub for ival].
+HB.instance Definition _ := [Equality of ivl by <:].
+HB.instance Definition _ := [Choice of ivl by <:].
 
 Definition low: ivl -> T := fst \o ival.
 Definition high: ivl -> T := snd \o ival.
@@ -754,9 +752,7 @@ rewrite H11 H12 ltxx eq_refl /=.
 by apply/le_trans/H22.
 Qed.
 
-Definition ivl_porderMixin : lePOrderMixin interval_eqType :=
-  LePOrderMixin lt_def_ivl refl_ivl anti_ivl trans_ivl.
-Canonical ivl_porderType := Eval hnf in POrderType tt ivl ivl_porderMixin.
+HB.instance Definition _ := Order.isPOrder.Build disp ivl lt_def_ivl refl_ivl anti_ivl trans_ivl.
 
 Fact total_ivl : total le_ivl.
 Proof.
@@ -765,14 +761,7 @@ case: (ltgtP (low x) (low y))=>//= _.
 by apply: le_total.
 Qed.
 
-Definition ivl_totalPOrderMixin :
-  totalPOrderMixin ivl_porderType := total_ivl.
-Canonical ivl_latticeType :=
-  Eval hnf in LatticeType ivl ivl_totalPOrderMixin.
-Canonical ivl_distrLatticeType :=
-  Eval hnf in DistrLatticeType ivl ivl_totalPOrderMixin.
-Canonical ivl_orderType :=
-  Eval hnf in OrderType ivl ivl_totalPOrderMixin.
+HB.instance Definition _ := Order.POrder_isTotal.Build disp ivl total_ivl.
 
 Definition overlap (x y : ivl) := (low y <= high x) && (low x <= high y).
 
@@ -811,12 +800,12 @@ elim: t=>/=; first by rewrite in_nil.
 move=>l IHl [a m] r IHr /and3P [/eqP -> /IHl Hl /IHr Hr] {IHl IHr}.
 rewrite mem_cat inE /max3; case/or3P.
 - move/Hl=>H.
-  apply/(le_trans H)/(le_trans (y:=Order.max (max_hi l) (max_hi r)));
-  by rewrite le_maxr lexx ?orbT.
-- by move/eqP=>->; rewrite le_maxr lexx.
+  apply/(le_trans H)/(le_trans (y:=Order.max (max_hi l) (max_hi r))) ;
+  by rewrite le_max lexx ?orbT.
+- by move/eqP=>->; rewrite le_max lexx.
 move/Hr=>H.
 apply/(le_trans H)/(le_trans (y:=Order.max (max_hi l) (max_hi r)));
-by rewrite le_maxr lexx ?orbT.
+by rewrite le_max lexx ?orbT.
 Qed.
 
 Lemma max_hi_mem t :

From 7d100609aaced50e1a85cfb5a0b184c1e9d16612 Mon Sep 17 00:00:00 2001
From: Timur Aminev <ablearthy@gmail.com>
Date: Sun, 5 Jan 2025 05:08:46 +0300
Subject: [PATCH 05/15] Update adt

---
 _CoqProject | 2 +-
 src/adt.v   | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index a11176c..6e2db24 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -8,7 +8,7 @@ src/sorting.v
 src/selection.v
 src/bintree.v
 src/bst.v
-# src/adt.v
+src/adt.v
 # src/twothree.v
 # src/redblack.v
 # src/avl.v
diff --git a/src/adt.v b/src/adt.v
index d5f9c1b..5c34086 100644
--- a/src/adt.v
+++ b/src/adt.v
@@ -37,7 +37,7 @@ Structure ASetM (T : eqType): Type :=
 End ASetM.
 
 Section Specification.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Corollary inorder_empty_pred : inorder (@Leaf T) =i pred0.
 Proof. by []. Qed.
@@ -187,7 +187,7 @@ End ASetI.
 (* Exercise 6.3 *)
 
 Section MapUnbalanced.
-Context {disp : unit} {K : orderType disp} {V : Type}.
+Context {disp : Order.disp_t} {K : orderType disp} {V : Type}.
 
 Notation kvtree := (tree (K*V)).
 

From 07f856e2787484b0d884274b95aa444b41c8012a Mon Sep 17 00:00:00 2001
From: Timur Aminev <ablearthy@gmail.com>
Date: Sun, 5 Jan 2025 05:13:30 +0300
Subject: [PATCH 06/15] Update twothree

---
 _CoqProject    |  2 +-
 src/twothree.v | 10 +++++-----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 6e2db24..07d9d56 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -9,7 +9,7 @@ src/selection.v
 src/bintree.v
 src/bst.v
 src/adt.v
-# src/twothree.v
+src/twothree.v
 # src/redblack.v
 # src/avl.v
 # src/beyond.v
diff --git a/src/twothree.v b/src/twothree.v
index 4d63cbc..c79defb 100644
--- a/src/twothree.v
+++ b/src/twothree.v
@@ -1,5 +1,6 @@
 From Equations Require Import Equations.
 From Coq Require Import ssreflect ssrbool ssrfun.
+From HB Require Import structures.
 From mathcomp Require Import ssrnat eqtype order seq path.
 From favssr Require Import prelude bst adt.
 
@@ -134,8 +135,7 @@ apply: (iffP and3P).
 by case=><-<-<-; split; [apply/IHl|apply/IHm|apply/IHr].
 Qed.
 
-Canonical tree23_eqMixin := EqMixin eqtree23P.
-Canonical tree23_eqType := Eval hnf in EqType (tree23 T) tree23_eqMixin.
+HB.instance Definition _ := hasDecEq.Build (tree23 T) eqtree23P.
 
 End EqType.
 
@@ -152,7 +152,7 @@ Proof.
 Admitted.
 
 Section SetImplementation.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Fixpoint isin23 (t : tree23 T) x : bool :=
   match t with
@@ -441,7 +441,7 @@ Definition delete (x : T) (t : tree23 T) : tree23 T :=
 End SetImplementation.
 
 Section PreservationOfCompleteness.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Definition hI {A} (u : upI A) : nat :=
   match u with
@@ -802,7 +802,7 @@ Proof. by exact: complete_treeD. Qed.
 End PreservationOfCompleteness.
 
 Section FunctionalCorrectness.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Definition bst_list (t : tree23 T) : bool := sorted <%O (inorder23 t).
 

From 7a225309aa15a8c28b6a07cb8faaee78ebea1886 Mon Sep 17 00:00:00 2001
From: Timur Aminev <ablearthy@gmail.com>
Date: Sun, 5 Jan 2025 05:15:32 +0300
Subject: [PATCH 07/15] Update redblack

---
 _CoqProject    | 2 +-
 src/redblack.v | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 07d9d56..439a716 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -10,7 +10,7 @@ src/bintree.v
 src/bst.v
 src/adt.v
 src/twothree.v
-# src/redblack.v
+src/redblack.v
 # src/avl.v
 # src/beyond.v
 # src/braun.v
diff --git a/src/redblack.v b/src/redblack.v
index eca087e..ee2e4b5 100644
--- a/src/redblack.v
+++ b/src/redblack.v
@@ -1,5 +1,6 @@
 From Equations Require Import Equations.
 From Coq Require Import ssreflect ssrbool ssrfun.
+From HB Require Import structures.
 From mathcomp Require Import eqtype ssrnat prime order seq path.
 From favssr Require Import prelude bintree bst adt.
 Set Implicit Arguments.
@@ -25,8 +26,7 @@ Definition eqcol (c1 c2 : col) :=
 Lemma eqcolP : Equality.axiom eqcol.
 Proof. by move; case; case; constructor. Qed.
 
-Canonical col_eqMixin := EqMixin eqcolP.
-Canonical col_eqType := Eval hnf in EqType col col_eqMixin.
+HB.instance Definition _ := hasDecEq.Build col eqcolP.
 
 Definition rbt A := tree (A * col).
 
@@ -146,7 +146,7 @@ End Invariants.
 Arguments invch_ind [A P].
 
 Section SetImplementation.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 (* insertion *)
 

From ec08077bb047278fc6a159c4ef2395654f1b9dfd Mon Sep 17 00:00:00 2001
From: Timur Aminev <ablearthy@gmail.com>
Date: Sun, 5 Jan 2025 05:22:17 +0300
Subject: [PATCH 08/15] Update avl

---
 _CoqProject |  2 +-
 src/avl.v   | 18 +++++++++---------
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 439a716..7b5900a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -11,7 +11,7 @@ src/bst.v
 src/adt.v
 src/twothree.v
 src/redblack.v
-# src/avl.v
+src/avl.v
 # src/beyond.v
 # src/braun.v
 # src/trie.v
diff --git a/src/avl.v b/src/avl.v
index ea37210..528da87 100644
--- a/src/avl.v
+++ b/src/avl.v
@@ -1,5 +1,6 @@
 From Equations Require Import Equations.
 From Coq Require Import ssreflect ssrbool ssrfun.
+From HB Require Import structures.
 From mathcomp Require Import eqtype ssrnat ssrint ssralg ssrnum order seq path.
 From favssr Require Import prelude bintree bst adt.
 Set Implicit Arguments.
@@ -149,15 +150,15 @@ Lemma fib_bound n : phi ^+ n <= (fib (n + 2)) %:R.
 Proof.
 funelim (fib n); simp fib=>//.
 - rewrite add0n; simp fib=>//; rewrite addn0 expr1 addn1 /phi.
-  rewrite -(@ler_pmul2r _ 2%:R) // mulfVK; last by rewrite pnatr_eq0.
-  rewrite -natrM (_ : (2*2 = 1+3)%N) // natrD mulr1n ler_add2l.
-  rewrite -(@ler_pexpn2r _ 2) //; first last.
+  rewrite -(@ler_pM2r _ 2%:R) // mulfVK; last by rewrite pnatr_eq0.
+  rewrite -natrM (_ : (2*2 = 1+3)%N) // natrD mulr1n lerD2l.
+  rewrite -(@ler_pXn2r _ 2) //; first last.
   - by rewrite nnegrE.
   - by rewrite nnegrE sqrtC_ge0; apply: ler0n.
   by rewrite sqrtCK expr2 -natrM ler_nat.
 rewrite -addn2 (addn2 (n + 2)); simp fib.
 rewrite exprD phi_sq mulrDr mulr1 natrD.
-by apply: ler_add=>//; move: H; rewrite exprD expr1 -!addnA.
+by apply: lerD=>//; move: H; rewrite exprD expr1 -!addnA.
 Qed.
 
 Corollary height_bound (t : tree_ht A) : avl t -> phi ^+ (height t) <= (size1_tree t)%:R.
@@ -174,7 +175,7 @@ Qed.
 End LogarithmicHeight.
 
 Section SetImplementation.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 (* rebalancing *)
 
@@ -741,7 +742,7 @@ Admitted.
 End Exercises.
 
 Section Optimization.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Variant bal := Lh | Bal | Rh.
 
@@ -756,8 +757,7 @@ Definition eqbal (b1 b2 : bal) :=
 Lemma eqbalP : Equality.axiom eqbal.
 Proof. by move; case; case; constructor. Qed.
 
-Canonical bal_eqMixin := EqMixin eqbalP.
-Canonical bal_eqType := Eval hnf in EqType bal bal_eqMixin.
+HB.instance Definition _ := hasDecEq.Build bal eqbalP.
 
 Definition tree_bal A := tree (A * bal).
 
@@ -1135,7 +1135,7 @@ Admitted.
 
 (* Exercise 9.7 *)
 
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Inductive tree4 A := Leaf
                    | Lh4 of (tree4 A) & A & (tree4 A)

From 2575dc2005c6ea8f311e077b011ebb98bd655d75 Mon Sep 17 00:00:00 2001
From: Timur Aminev <ablearthy@gmail.com>
Date: Sun, 5 Jan 2025 05:23:46 +0300
Subject: [PATCH 09/15] Update beyond

---
 _CoqProject  |  2 +-
 src/beyond.v | 12 ++++++------
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 7b5900a..4fb0486 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -12,7 +12,7 @@ src/adt.v
 src/twothree.v
 src/redblack.v
 src/avl.v
-# src/beyond.v
+src/beyond.v
 # src/braun.v
 # src/trie.v
 # src/quadtree.v
diff --git a/src/beyond.v b/src/beyond.v
index 20bd01c..3a24495 100644
--- a/src/beyond.v
+++ b/src/beyond.v
@@ -13,7 +13,7 @@ Open Scope order_scope.
 
 (* TODO switch to packed structures to reuse ASetM *)
 Module ASetM2.
-Structure ASetM2 (disp : unit) (T : orderType disp): Type :=
+Structure ASetM2 (disp : Order.disp_t) (T : orderType disp): Type :=
   make {tp :> Type;
         empty : tp;
         insert : T -> tp -> tp;
@@ -54,7 +54,7 @@ Structure ASetM2 (disp : unit) (T : orderType disp): Type :=
 End ASetM2.
 
 (* TODO use a canonical structure? *)
-Structure JoinSig (disp : unit) (X : orderType disp) (Y : Type) : Type :=
+Structure JoinSig (disp : Order.disp_t) (X : orderType disp) (Y : Type) : Type :=
   mkjoin {
     join : tree (X*Y) -> X -> tree (X*Y) -> tree (X*Y);
     inv : tree (X*Y) -> bool;
@@ -70,7 +70,7 @@ Structure JoinSig (disp : unit) (X : orderType disp) (Y : Type) : Type :=
 }.
 
 Section JustJoin.
-Context {disp : unit} {X : orderType disp} {Y : Type} {j : JoinSig X Y}.
+Context {disp : Order.disp_t} {X : orderType disp} {Y : Type} {j : JoinSig X Y}.
 
 Fixpoint split (t : tree (X*Y)) (x : X) : (tree (X*Y) * bool * tree (X*Y)) :=
   if t is Node l (a,_) r then
@@ -465,7 +465,7 @@ Admitted.
 End JustJoin.
 
 Section JoiningRedBlackTrees.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Lemma ne_bhgt (t1 t2 : rbt T) : non_empty_if (bh t1 < bh t2)%N t2.
 Proof.
@@ -773,7 +773,7 @@ Definition JoinRBT :=
 End JoiningRedBlackTrees.
 
 Section RBTSetJoin.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Definition invariant' (t : rbt T) := bst_list_a t && invch t.
 
@@ -888,7 +888,7 @@ End RBTSetJoin.
 From favssr Require Import twothree.
 
 Section Joining23Trees.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Equations? join23L (l : tree23 T) (x : T) (r : tree23 T) : upI T by wf (size23 r) lt :=
 join23L l x r => TI l. (* FIXME *)

From c88ad404b003a15cbf846f5e580ca7c5c132c6bf Mon Sep 17 00:00:00 2001
From: Timur Aminev <ablearthy@gmail.com>
Date: Sun, 5 Jan 2025 05:26:26 +0300
Subject: [PATCH 10/15] Minor updates

---
 _CoqProject    | 10 +++++-----
 src/leftist.v  |  8 ++++----
 src/priority.v |  8 ++++----
 3 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 4fb0486..1fb65b1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -13,11 +13,11 @@ src/twothree.v
 src/redblack.v
 src/avl.v
 src/beyond.v
-# src/braun.v
-# src/trie.v
-# src/quadtree.v
-# src/priority.v
-# src/leftist.v
+src/braun.v
+src/trie.v
+src/quadtree.v
+src/priority.v
+src/leftist.v
 # src/braun_queue.v
 # src/binom_heap.v
 # src/huffman.v
\ No newline at end of file
diff --git a/src/leftist.v b/src/leftist.v
index d250202..205b4bb 100644
--- a/src/leftist.v
+++ b/src/leftist.v
@@ -11,7 +11,7 @@ Import Order.TotalTheory.
 Open Scope order_scope.
 
 Section Intro.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Definition lheap T := tree (T * nat).
 
@@ -43,7 +43,7 @@ Admitted.
 End Intro.
 
 Section ImplementationPQM.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Definition empty_lheap : lheap T := leaf.
 
@@ -76,7 +76,7 @@ Definition del_min (t : lheap T) : lheap T :=
 End ImplementationPQM.
 
 Section Correctness.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Definition mset_lheap (h : lheap T) : seq T := preorder_a h.
 
@@ -244,7 +244,7 @@ Definition LHeapPQM :=
 End Correctness.
 
 Section RunningTimeAnalysis.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Fixpoint T_merge (h1 : lheap T) : lheap T -> nat :=
   if h1 is Node l1 (a1,_) r1 then
diff --git a/src/priority.v b/src/priority.v
index 24cd9cb..ec50c29 100644
--- a/src/priority.v
+++ b/src/priority.v
@@ -11,7 +11,7 @@ Import Order.TotalTheory.
 Open Scope order_scope.
 
 Module APQ.
-Structure APQ (disp : unit) (T : orderType disp): Type :=
+Structure APQ (disp : Order.disp_t) (T : orderType disp): Type :=
   make {tp :> Type;
         empty : tp;
         insert : T -> tp -> tp;
@@ -39,7 +39,7 @@ Structure APQ (disp : unit) (T : orderType disp): Type :=
 End APQ.
 
 Module APQM.
-Structure APQ (disp : unit) (T : orderType disp): Type :=
+Structure APQ (disp : Order.disp_t) (T : orderType disp): Type :=
   make {tp :> Type;
         empty : tp;
         insert : T -> tp -> tp;
@@ -73,7 +73,7 @@ End APQM.
 
 (* Exercise 14.1 *)
 Section Exercise.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Definition empty_list : seq T := [::].
 
@@ -99,7 +99,7 @@ Definition ListPQM :=
 End Exercise.
 
 Section Heaps.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Fixpoint heap (t : tree T) : bool :=
   if t is Node l m r

From 14863ec14d42e5bbdcd4bae57ca23da1875ee053 Mon Sep 17 00:00:00 2001
From: Timur Aminev <ablearthy@gmail.com>
Date: Sun, 5 Jan 2025 05:27:06 +0300
Subject: [PATCH 11/15] Update braun_queue

---
 _CoqProject       | 2 +-
 src/braun_queue.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 1fb65b1..3cd3d9f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -18,6 +18,6 @@ src/trie.v
 src/quadtree.v
 src/priority.v
 src/leftist.v
-# src/braun_queue.v
+src/braun_queue.v
 # src/binom_heap.v
 # src/huffman.v
\ No newline at end of file
diff --git a/src/braun_queue.v b/src/braun_queue.v
index 795d60d..f4438eb 100644
--- a/src/braun_queue.v
+++ b/src/braun_queue.v
@@ -12,7 +12,7 @@ Import Order.TotalTheory.
 Open Scope order_scope.
 
 Section Implementation.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Fixpoint insert (a : T) (t : tree T) : tree T :=
   if t is Node l x r then
@@ -59,7 +59,7 @@ Definition del_min (t : tree T) : tree T :=
 End Implementation.
 
 Section Correctness.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Lemma size_insert (x : T) t : size_tree (insert x t) = size_tree t + 1.
 Proof.

From df2bbe3de13483ecb649c0390e684b1f70ba3b43 Mon Sep 17 00:00:00 2001
From: Timur Aminev <ablearthy@gmail.com>
Date: Sun, 5 Jan 2025 05:29:09 +0300
Subject: [PATCH 12/15] Update binom_heap

---
 _CoqProject      |  2 +-
 src/binom_heap.v | 16 ++++++++--------
 2 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 3cd3d9f..5ef17c7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -19,5 +19,5 @@ src/quadtree.v
 src/priority.v
 src/leftist.v
 src/braun_queue.v
-# src/binom_heap.v
+src/binom_heap.v
 # src/huffman.v
\ No newline at end of file
diff --git a/src/binom_heap.v b/src/binom_heap.v
index 682812f..f468500 100644
--- a/src/binom_heap.v
+++ b/src/binom_heap.v
@@ -1,5 +1,6 @@
 From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype order seq path bigop prime binomial.
+From HB Require Import structures.
 From favssr Require Import prelude basics priority.
 
 Set Implicit Arguments.
@@ -68,8 +69,7 @@ rewrite {}H12; case: H2.
 by move=>H12; apply: ReflectF; case=>E; rewrite E in H12.
 Qed.
 
-Canonical tree_eqMixin := EqMixin eqtreeP.
-Canonical tree_eqType := Eval hnf in EqType (tree A) tree_eqMixin.
+HB.instance Definition _ := hasDecEq.Build (tree A) eqtreeP.
 
 Lemma tree_ind_eq (P : tree A -> Prop) :
   (forall r a l, (forall x, x \in l -> P x) -> P (Node r a l)) ->
@@ -83,7 +83,7 @@ Qed.
 End TreeEq.
 
 Section TreeOrd.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Fixpoint invar_btree (t : tree T) : bool :=
   let: Node r _ ts := t in
@@ -116,7 +116,7 @@ Qed.
 End TreeOrd.
 
 Section Size.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Fixpoint mset_tree (t : tree T) : seq T :=
   let: Node _ a ts := t in
@@ -226,7 +226,7 @@ Qed.
 End Size.
 
 Section PriorityQueueImplementation.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 (* insert *)
 
@@ -431,7 +431,7 @@ elim: h t=>/=.
 - move=>t Ht _ _; rewrite mset_heap_nil in_nil orbF=>Hx.
   by apply: invar_tree_root_min.
 move=>t1 ts IH t Ht _.
-rewrite invar_cons; case/and3P=>Ht1 Ha1 Hs; rewrite le_minl; case/orP.
+rewrite invar_cons; case/and3P=>Ht1 Ha1 Hs; rewrite ge_min; case/orP.
 - by move=>Hx; rewrite invar_tree_root_min.
 rewrite mset_heap_cons mem_cat=>Hx.
 by rewrite IH // orbT.
@@ -597,7 +597,7 @@ Definition BHeapPQM :=
 End PriorityQueueImplementation.
 
 Section RunningTimeAnalysis.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 Definition T_link (t1 t2 : tree T) : nat := 1.
 
@@ -749,7 +749,7 @@ Qed.
 End RunningTimeAnalysis.
 
 Section Exercises.
-Context {disp : unit} {T : orderType disp}.
+Context {disp : Order.disp_t} {T : orderType disp}.
 
 (* Exercise 17.1 *)
 

From 451b7e6b7297a74f7a2d3b54d4adf601774713af Mon Sep 17 00:00:00 2001
From: Timur Aminev <ablearthy@gmail.com>
Date: Sun, 5 Jan 2025 05:30:29 +0300
Subject: [PATCH 13/15] Update huffman

---
 _CoqProject   | 2 +-
 src/huffman.v | 5 ++---
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 5ef17c7..6ba87fa 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -20,4 +20,4 @@ src/priority.v
 src/leftist.v
 src/braun_queue.v
 src/binom_heap.v
-# src/huffman.v
\ No newline at end of file
+src/huffman.v
\ No newline at end of file
diff --git a/src/huffman.v b/src/huffman.v
index ca2c4f7..eb2199f 100644
--- a/src/huffman.v
+++ b/src/huffman.v
@@ -1,5 +1,6 @@
 From Equations Require Import Equations.
 From Coq Require Import ssreflect ssrbool ssrfun.
+From HB Require Import structures.
 From mathcomp Require Import eqtype ssrnat seq bigop ssrAC.
 From favssr Require Import prelude.
 
@@ -69,9 +70,7 @@ have [<-/=|neqx] := w1 =P w2; last by apply: ReflectF; case.
 by case=><-<-; split; [apply/IHl|apply/IHr].
 Qed.
 
-Canonical tree_eqMixin := EqMixin eqtreeP.
-Canonical tree_eqType := Eval hnf in EqType (tree T) tree_eqMixin.
-
+HB.instance Definition _ := hasDecEq.Build (tree T) eqtreeP.
 End EqTree.
 
 Section BasicAuxiliaryFunctions.

From d272f3728cf4b4059e78db28226dbeaeaa07e5d7 Mon Sep 17 00:00:00 2001
From: Timur Aminev <ablearthy@gmail.com>
Date: Sun, 5 Jan 2025 05:37:55 +0300
Subject: [PATCH 14/15] Update versions

---
 .github/workflows/docker-action.yml | 11 +++++------
 README.md                           |  4 ++--
 coq-fav-ssr.opam                    |  4 ++--
 meta.yml                            | 18 +++++++++---------
 4 files changed, 18 insertions(+), 19 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 80b2e23..f8b5549 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -17,12 +17,11 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.19.0-coq-8.20'
-          - 'mathcomp/mathcomp:1.19.0-coq-8.19'
-          - 'mathcomp/mathcomp:1.18.0-coq-8.18'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.15'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.20'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.16'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3
diff --git a/README.md b/README.md
index de162a2..c77822a 100644
--- a/README.md
+++ b/README.md
@@ -34,9 +34,9 @@ The book was previously called "Functional Algorithms Verified", hence the FAV a
 - Coq-community maintainer(s):
   - Alex Gryzlov ([**@clayrat**](https://github.com/clayrat))
 - License: [MIT license](LICENSE)
-- Compatible Coq versions: 8.15 to 8.19
+- Compatible Coq versions: 8.16 to 8.20
 - Additional dependencies:
-  - [MathComp ssreflect](https://math-comp.github.io) 1.17.0 to 1.19.0
+  - [MathComp ssreflect](https://math-comp.github.io) 2.2 to 2.3
   - [MathComp algebra](https://math-comp.github.io)
   - [Equations](https://github.com/mattam82/Coq-Equations) 1.3 or later
 - Coq namespace: `favssr`
diff --git a/coq-fav-ssr.opam b/coq-fav-ssr.opam
index 1a99b0d..cc37f49 100644
--- a/coq-fav-ssr.opam
+++ b/coq-fav-ssr.opam
@@ -19,8 +19,8 @@ The book was previously called "Functional Algorithms Verified", hence the FAV a
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.15" & < "8.21"}
-  "coq-mathcomp-ssreflect" {>= "1.17" & < "2.0"}
+  "coq" {>= "8.16" & < "8.21"}
+  "coq-mathcomp-ssreflect" {>= "2.2" & < "2.4"}
   "coq-mathcomp-algebra" 
   "coq-equations" {>= "1.3"}
 ]
diff --git a/meta.yml b/meta.yml
index b55eb4c..5a1425d 100644
--- a/meta.yml
+++ b/meta.yml
@@ -32,27 +32,27 @@ license:
   identifier: MIT
 
 supported_coq_versions:
-  text: 8.15 to 8.20
-  opam: '{>= "8.15" & < "8.21"}'
+  text: 8.16 to 8.20
+  opam: '{>= "8.16" & < "8.21"}'
 
 tested_coq_opam_versions:
-- version: '1.19.0-coq-8.19'
+- version: '2.3.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
-- version: '1.18.0-coq-8.18'
+- version: '2.3.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.17'
+- version: '2.3.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.16'
+- version: '2.2.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.15'
+- version: '2.2.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{>= "1.17" & < "2.0"}'
+    version: '{>= "2.2" & < "2.4"}'
   description: |-
-    [MathComp ssreflect](https://math-comp.github.io) 1.17.0 to 1.19.0
+    [MathComp ssreflect](https://math-comp.github.io) 2.2 to 2.3
 - opam:
     name: coq-mathcomp-algebra
   description: |-

From 3998099dc7de590bf9358ee37e97c581343e4b01 Mon Sep 17 00:00:00 2001
From: Timur Aminev <ablearthy@gmail.com>
Date: Sun, 5 Jan 2025 05:49:52 +0300
Subject: [PATCH 15/15] Remove mathcomp 2.2

---
 .github/workflows/docker-action.yml |  2 --
 README.md                           |  4 ++--
 coq-fav-ssr.opam                    |  4 ++--
 meta.yml                            | 12 ++++--------
 4 files changed, 8 insertions(+), 14 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index f8b5549..0abec96 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -20,8 +20,6 @@ jobs:
           - 'mathcomp/mathcomp:2.3.0-coq-8.20'
           - 'mathcomp/mathcomp:2.3.0-coq-8.19'
           - 'mathcomp/mathcomp:2.3.0-coq-8.18'
-          - 'mathcomp/mathcomp:2.2.0-coq-8.17'
-          - 'mathcomp/mathcomp:2.2.0-coq-8.16'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3
diff --git a/README.md b/README.md
index c77822a..d353e2f 100644
--- a/README.md
+++ b/README.md
@@ -34,9 +34,9 @@ The book was previously called "Functional Algorithms Verified", hence the FAV a
 - Coq-community maintainer(s):
   - Alex Gryzlov ([**@clayrat**](https://github.com/clayrat))
 - License: [MIT license](LICENSE)
-- Compatible Coq versions: 8.16 to 8.20
+- Compatible Coq versions: 8.18 to 8.20
 - Additional dependencies:
-  - [MathComp ssreflect](https://math-comp.github.io) 2.2 to 2.3
+  - [MathComp ssreflect](https://math-comp.github.io) 2.3
   - [MathComp algebra](https://math-comp.github.io)
   - [Equations](https://github.com/mattam82/Coq-Equations) 1.3 or later
 - Coq namespace: `favssr`
diff --git a/coq-fav-ssr.opam b/coq-fav-ssr.opam
index cc37f49..da512a7 100644
--- a/coq-fav-ssr.opam
+++ b/coq-fav-ssr.opam
@@ -19,8 +19,8 @@ The book was previously called "Functional Algorithms Verified", hence the FAV a
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.16" & < "8.21"}
-  "coq-mathcomp-ssreflect" {>= "2.2" & < "2.4"}
+  "coq" {>= "8.18" & < "8.21"}
+  "coq-mathcomp-ssreflect" {>= "2.3" & < "2.4"}
   "coq-mathcomp-algebra" 
   "coq-equations" {>= "1.3"}
 ]
diff --git a/meta.yml b/meta.yml
index 5a1425d..f2df206 100644
--- a/meta.yml
+++ b/meta.yml
@@ -32,8 +32,8 @@ license:
   identifier: MIT
 
 supported_coq_versions:
-  text: 8.16 to 8.20
-  opam: '{>= "8.16" & < "8.21"}'
+  text: 8.18 to 8.20
+  opam: '{>= "8.18" & < "8.21"}'
 
 tested_coq_opam_versions:
 - version: '2.3.0-coq-8.20'
@@ -42,17 +42,13 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '2.3.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{>= "2.2" & < "2.4"}'
+    version: '{>= "2.3" & < "2.4"}'
   description: |-
-    [MathComp ssreflect](https://math-comp.github.io) 2.2 to 2.3
+    [MathComp ssreflect](https://math-comp.github.io) 2.3.0
 - opam:
     name: coq-mathcomp-algebra
   description: |-