diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 55a353e..9365ab7 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -20,7 +20,7 @@ jobs:
     - name: Run minimizer
       uses: coq-community/docker-coq-action@v1.4.1
       with:
-        #custom_image: 'registry.gitlab.com/coq/coq:CACHEKEY'
+        custom_image: 'registry.gitlab.inria.fr/coq/coq:edge_ubuntu-V2023-08-28-93124ee272'
         #coq_version: 'latest'
         #ocaml_version: 'default'
         custom_script: ./timeout-run.sh
diff --git a/bug.v b/bug.v
new file mode 100644
index 0000000..e0db885
--- /dev/null
+++ b/bug.v
@@ -0,0 +1,3186 @@
+
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-projection-no-head-constant" "-w" "-redundant-canonical-projection" "-w" "-notation-overridden" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/oddorder/theories" "odd_order" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/HB" "HB" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/elpi" "elpi" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/mathcomp" "mathcomp" "-top" "Top.bug_01") -*- *)
+(* File reduced by coq-bug-minimizer from original input, then from 1375 lines to 60 lines, then from 73 lines to 1675 lines, then from 1680 lines to 90 lines, then from 103 lines to 2712 lines, then from 2715 lines to 148 lines, then from 161 lines to 2932 lines, then from 2936 lines to 147 lines, then from 160 lines to 1746 lines, then from 1749 lines to 189 lines, then from 202 lines to 1254 lines, then from 1259 lines to 145 lines, then from 158 lines to 976 lines, then from 981 lines to 153 lines, then from 166 lines to 775 lines, then from 779 lines to 245 lines, then from 239 lines to 175 lines, then from 188 lines to 604 lines, then from 609 lines to 168 lines, then from 181 lines to 1580 lines, then from 1585 lines to 231 lines, then from 244 lines to 1254 lines, then from 1259 lines to 261 lines, then from 274 lines to 1855 lines, then from 1859 lines to 261 lines, then from 274 lines to 3310 lines, then from 3315 lines to 2052 lines, then from 1806 lines to 484 lines, then from 497 lines to 2159 lines, then from 2164 lines to 571 lines, then from 584 lines to 3152 lines, then from 3155 lines to 2910 lines, then from 2767 lines to 646 lines, then from 659 lines to 3393 lines, then from 3398 lines to 3162 lines, then from 3016 lines to 743 lines, then from 756 lines to 1264 lines, then from 1269 lines to 933 lines, then from 879 lines to 827 lines, then from 840 lines to 1556 lines, then from 1561 lines to 927 lines, then from 940 lines to 3367 lines, then from 3371 lines to 3182 lines *)
+(* coqc version 8.19+alpha compiled with OCaml 4.14.1
+   coqtop version 728713d43dde:/builds/coq/coq/_build/default,(HEAD detached at 25e3b11) (25e3b11cee094cfce7e16d10e58d3b7b318ea70c)
+   Expected coqc runtime on this file: 8.069 sec *)
+Require Coq.Init.Ltac.
+Require Coq.Bool.Bool.
+Require Coq.Floats.PrimFloat.
+Require Coq.NArith.BinNat.
+Require Coq.NArith.Ndec.
+Require Coq.Numbers.Cyclic.Int63.PrimInt63.
+Require Coq.PArith.BinPos.
+Require Coq.Strings.String.
+Require Coq.setoid_ring.Ring.
+Require Coq.ssr.ssrbool.
+Require Coq.ssr.ssreflect.
+Require Coq.ssr.ssrfun.
+Require mathcomp.ssreflect.ssrnotations.
+Require mathcomp.ssreflect.ssreflect.
+Require elpi.elpi.
+Require mathcomp.ssreflect.ssrfun.
+Require mathcomp.ssreflect.ssrbool.
+Require HB.structures.
+Require mathcomp.ssreflect.eqtype.
+Require mathcomp.ssreflect.ssrnat.
+Require mathcomp.ssreflect.seq.
+Require mathcomp.ssreflect.choice.
+Require mathcomp.ssreflect.div.
+Require mathcomp.ssreflect.path.
+
+Module Export AdmitTactic.
+Module Import LocalFalse.
+Inductive False : Prop := .
+End LocalFalse.
+Axiom proof_admitted : False.
+Import Coq.Init.Ltac.
+Tactic Notation "admit" := abstract case proof_admitted.
+End AdmitTactic.
+
+Module mathcomp_DOT_ssreflect_DOT_fintype_WRAPPED.
+Module fintype.
+ 
+ 
+Import HB.structures.
+Import mathcomp.ssreflect.ssreflect mathcomp.ssreflect.ssrfun mathcomp.ssreflect.ssrbool mathcomp.ssreflect.eqtype mathcomp.ssreflect.ssrnat mathcomp.ssreflect.seq mathcomp.ssreflect.choice.
+Import mathcomp.ssreflect.path mathcomp.ssreflect.div.
+
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Declare Scope fin_quant_scope.
+
+Definition finite_axiom (T : eqType) e :=
+  forall x : T, count_mem x e = 1.
+
+HB.mixin Record isFinite T of Equality T := {
+  enum_subdef : seq T;
+  enumP_subdef : finite_axiom enum_subdef
+}.
+
+#[short(type="finType")]
+HB.structure Definition Finite := {T of isFinite T & Countable T }.
+
+Module Export FiniteNES.
+Module Finite.
+
+HB.lock Definition enum T := isFinite.enum_subdef (Finite.class T).
+
+Notation axiom := finite_axiom.
+#[deprecated(since="mathcomp 2.0.0", note="Use isFinite.Build instead.")]
+Notation EnumMixin m := (@isFinite.Build _ _ m).
+
+Lemma uniq_enumP (T : eqType) e : uniq e -> e =i T -> axiom e.
+Proof.
+by move=> Ue sT x; rewrite count_uniq_mem ?sT.
+Qed.
+
+Section WithCountType.
+Variable (T : countType).
+
+Definition UniqMixin_deprecated e Ue (eT : e =i T) :=
+  @isFinite.Build T e (uniq_enumP Ue eT).
+
+Variable n : nat.
+
+Definition count_enum := pmap (@pickle_inv T) (iota 0 n).
+
+Hypothesis ubT : forall x : T, pickle x < n.
+
+Lemma count_enumP : axiom count_enum.
+Proof.
+apply: uniq_enumP (pmap_uniq (@pickle_invK T) (iota_uniq _ _)) _ => x.
+by rewrite mem_pmap -pickleK_inv map_f // mem_iota ubT.
+Qed.
+
+Definition CountMixin_deprecated := @isFinite.Build _ _ count_enumP.
+
+End WithCountType.
+#[deprecated(since="mathcomp 2.0.0",
+  note="Use isFinite.Build and Finite.uniq_enumP instead.")]
+Notation UniqMixin := UniqMixin_deprecated.
+#[deprecated(since="mathcomp 2.0.0",
+  note="Use isFinite.Build and Finite.count_enumP instead.")]
+Notation CountMixin := CountMixin_deprecated.
+End Finite.
+Canonical finEnum_unlock := Unlockable Finite.enum.unlock.
+End FiniteNES.
+
+Section CanonicalFinType.
+Variable (T : eqType) (s : seq T).
+
+Definition fin_type of finite_axiom s : Type := T.
+
+Variable (f : finite_axiom s).
+Notation fT := (fin_type f).
+
+Definition fin_pickle (x : fT) : nat := index x s.
+Definition fin_unpickle (n : nat) : option fT :=
+  nth None (map some s) n.
+Lemma fin_pickleK : pcancel fin_pickle fin_unpickle.
+Proof.
+move=> x; rewrite /fin_pickle/fin_unpickle.
+rewrite -(index_map Some_inj) nth_index ?map_f//.
+by apply/count_memPn=> /eqP; rewrite f.
+Qed.
+
+HB.instance Definition _ := Equality.on fT.
+HB.instance Definition _ := isCountable.Build fT fin_pickleK.
+HB.instance Definition _ := isFinite.Build fT f.
+
+End CanonicalFinType.
+
+#[deprecated(since="mathcomp 2.0.0", note="Use isFinite.Build instead.")]
+Notation FinMixin x := (@isFinite.Build _ _ x).
+#[deprecated(since="mathcomp 2.0.0",
+  note="Use isFinite.Build with Finite.uniq_enumP instead.")]
+Notation UniqFinMixin := Finite.UniqMixin_deprecated.
+#[deprecated(since="mathcomp 2.0.0", note="Use Finite.clone instead.")]
+Notation "[ 'finType' 'of' T 'for' cT ]" := (Finite.clone T%type cT)
+  (at level 0, format "[ 'finType'  'of'  T  'for'  cT ]") : form_scope.
+#[deprecated(since="mathcomp 2.0.0", note="Use Finite.clone instead.")]
+Notation "[ 'finType' 'of' T ]" := (Finite.clone T%type _)
+  (at level 0, format "[ 'finType'  'of'  T ]") : form_scope.
+
+ 
+ 
+ 
+Definition fin_pred_sort (T : finType) (pT : predType T) := pred_sort pT.
+Identity Coercion pred_sort_of_fin : fin_pred_sort >-> pred_sort.
+
+Definition enum_mem T (mA : mem_pred _) := filter mA (Finite.enum T).
+Notation enum A := (enum_mem (mem A)).
+Definition pick (T : finType) (P : pred T) := ohead (enum P).
+
+Notation "[ 'pick' x | P ]" := (pick (fun x => P%B))
+  (at level 0, x name, format "[ 'pick'  x  |  P  ]") : form_scope.
+Notation "[ 'pick' x : T | P ]" := (pick (fun x : T => P%B))
+  (at level 0, x name, only parsing) : form_scope.
+Definition pick_true T (x : T) := true.
+Reserved Notation "[ 'pick' x : T ]"
+  (at level 0, x name, format "[ 'pick'  x : T ]").
+Notation "[ 'pick' x : T ]" := [pick x : T | pick_true x]
+  (only parsing) : form_scope.
+Notation "[ 'pick' x : T ]" := [pick x : T | pick_true _]
+  (only printing) : form_scope.
+Notation "[ 'pick' x ]" := [pick x : _]
+  (at level 0, x name, only parsing) : form_scope.
+Notation "[ 'pick' x | P & Q ]" := [pick x | P && Q ]
+  (at level 0, x name,
+   format "[ '[hv ' 'pick'  x  |  P '/ '   &  Q ] ']'") : form_scope.
+Notation "[ 'pick' x : T | P & Q ]" := [pick x : T | P && Q ]
+  (at level 0, x name, only parsing) : form_scope.
+Notation "[ 'pick' x 'in' A ]" := [pick x | x \in A]
+  (at level 0, x name, format "[ 'pick'  x  'in'  A  ]") : form_scope.
+Notation "[ 'pick' x : T 'in' A ]" := [pick x : T | x \in A]
+  (at level 0, x name, only parsing) : form_scope.
+Notation "[ 'pick' x 'in' A | P ]" := [pick x | x \in A & P ]
+  (at level 0, x name,
+   format "[ '[hv ' 'pick'  x  'in'  A '/ '   |  P ] ']'") : form_scope.
+Notation "[ 'pick' x : T 'in' A | P ]" := [pick x : T | x \in A & P ]
+  (at level 0, x name, only parsing) : form_scope.
+Notation "[ 'pick' x 'in' A | P & Q ]" := [pick x in A | P && Q]
+  (at level 0, x name, format
+  "[ '[hv ' 'pick'  x  'in'  A '/ '   |  P '/ '  &  Q ] ']'") : form_scope.
+Notation "[ 'pick' x : T 'in' A | P & Q ]" := [pick x : T in A | P && Q]
+  (at level 0, x name, only parsing) : form_scope.
+
+ 
+ 
+HB.lock Definition card (T : finType) (mA : mem_pred T) := size (enum_mem mA).
+Canonical card_unlock := Unlockable card.unlock.
+
+ 
+Notation "#| A |" := (card (mem A))
+  (at level 0, A at level 99, format "#| A |") : nat_scope.
+
+Definition pred0b (T : finType) (P : pred T) := #|P| == 0.
+Prenex Implicits pred0b.
+
+Module FiniteQuant.
+
+Variant quantified := Quantified of bool.
+
+Delimit Scope fin_quant_scope with Q.
+ 
+Bind Scope fin_quant_scope with quantified.
+
+Notation "F ^*" := (Quantified F) (at level 2).
+Notation "F ^~" := (~~ F) (at level 2).
+
+Section Definitions.
+
+Variable T : finType.
+Implicit Types (B : quantified) (x y : T).
+
+Definition quant0b Bp := pred0b [pred x : T | let: F^* := Bp x x in F].
+ 
+ 
+Definition ex B x y := B.
+ 
+ 
+Definition all B x y := let: F^* := B in F^~^*.
+Definition all_in C B x y := let: F^* := B in (C ==> F)^~^*.
+Definition ex_in C B x y :=  let: F^* := B in (C && F)^*.
+
+End Definitions.
+
+Notation "[ x | B ]" := (quant0b (fun x => B x)) (at level 0, x name).
+Notation "[ x : T | B ]" := (quant0b (fun x : T => B x)) (at level 0, x name).
+
+Module Exports.
+
+Notation ", F" := F^* (at level 200, format ", '/ '  F") : fin_quant_scope.
+
+Notation "[ 'forall' x B ]" := [x | all B]
+  (at level 0, x at level 99, B at level 200,
+   format "[ '[hv' 'forall'  x B ] ']'") : bool_scope.
+
+Notation "[ 'forall' x : T B ]" := [x : T | all B]
+  (at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
+Notation "[ 'forall' ( x | C ) B ]" := [x | all_in C B]
+  (at level 0, x at level 99, B at level 200,
+   format "[ '[hv' '[' 'forall'  ( x '/  '  |  C ) ']' B ] ']'") : bool_scope.
+Notation "[ 'forall' ( x : T | C ) B ]" := [x : T | all_in C B]
+  (at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
+Notation "[ 'forall' x 'in' A B ]" := [x | all_in (x \in A) B]
+  (at level 0, x at level 99, B at level 200,
+   format "[ '[hv' '[' 'forall'  x '/  '  'in'  A ']' B ] ']'") : bool_scope.
+Notation "[ 'forall' x : T 'in' A B ]" := [x : T | all_in (x \in A) B]
+  (at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
+Notation ", 'forall' x B" := [x | all B]^*
+  (at level 200, x at level 99, B at level 200,
+   format ", '/ '  'forall'  x B") : fin_quant_scope.
+Notation ", 'forall' x : T B" := [x : T | all B]^*
+  (at level 200, x at level 99, B at level 200, only parsing) : fin_quant_scope.
+Notation ", 'forall' ( x | C ) B" := [x | all_in C B]^*
+  (at level 200, x at level 99, B at level 200,
+   format ", '/ '  '[' 'forall'  ( x '/  '  |  C ) ']' B") : fin_quant_scope.
+Notation ", 'forall' ( x : T | C ) B" := [x : T | all_in C B]^*
+  (at level 200, x at level 99, B at level 200, only parsing) : fin_quant_scope.
+Notation ", 'forall' x 'in' A B" := [x | all_in (x \in A) B]^*
+  (at level 200, x at level 99, B at level 200,
+   format ", '/ '  '[' 'forall'  x '/  '  'in'  A ']' B") : bool_scope.
+Notation ", 'forall' x : T 'in' A B" := [x : T | all_in (x \in A) B]^*
+  (at level 200, x at level 99, B at level 200, only parsing) : bool_scope.
+
+Notation "[ 'exists' x B ]" := [x | ex B]^~
+  (at level 0, x at level 99, B at level 200,
+   format "[ '[hv' 'exists'  x B ] ']'") : bool_scope.
+Notation "[ 'exists' x : T B ]" := [x : T | ex B]^~
+  (at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
+Notation "[ 'exists' ( x | C ) B ]" := [x | ex_in C B]^~
+  (at level 0, x at level 99, B at level 200,
+   format "[ '[hv' '[' 'exists'  ( x '/  '  |  C ) ']' B ] ']'") : bool_scope.
+Notation "[ 'exists' ( x : T | C ) B ]" := [x : T | ex_in C B]^~
+  (at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
+Notation "[ 'exists' x 'in' A B ]" := [x | ex_in (x \in A) B]^~
+  (at level 0, x at level 99, B at level 200,
+   format "[ '[hv' '[' 'exists'  x '/  '  'in'  A ']' B ] ']'") : bool_scope.
+Notation "[ 'exists' x : T 'in' A B ]" := [x : T | ex_in (x \in A) B]^~
+  (at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
+Notation ", 'exists' x B" := [x | ex B]^~^*
+  (at level 200, x at level 99, B at level 200,
+   format ", '/ '  'exists'  x B") : fin_quant_scope.
+Notation ", 'exists' x : T B" := [x : T | ex B]^~^*
+  (at level 200, x at level 99, B at level 200, only parsing) : fin_quant_scope.
+Notation ", 'exists' ( x | C ) B" := [x | ex_in C B]^~^*
+  (at level 200, x at level 99, B at level 200,
+   format ", '/ '  '[' 'exists'  ( x '/  '  |  C ) ']' B") : fin_quant_scope.
+Notation ", 'exists' ( x : T | C ) B" := [x : T | ex_in C B]^~^*
+  (at level 200, x at level 99, B at level 200, only parsing) : fin_quant_scope.
+Notation ", 'exists' x 'in' A B" := [x | ex_in (x \in A) B]^~^*
+  (at level 200, x at level 99, B at level 200,
+   format ", '/ '  '[' 'exists'  x '/  '  'in'  A ']' B") : bool_scope.
+Notation ", 'exists' x : T 'in' A B" := [x : T | ex_in (x \in A) B]^~^*
+  (at level 200, x at level 99, B at level 200, only parsing) : bool_scope.
+
+End Exports.
+
+End FiniteQuant.
+Export FiniteQuant.Exports.
+
+Definition disjoint T (A B : mem_pred _) := @pred0b T (predI A B).
+Notation "[ 'disjoint' A & B ]" := (disjoint (mem A) (mem B))
+  (at level 0,
+   format "'[hv' [ 'disjoint' '/  '  A '/'  &  B ] ']'") : bool_scope.
+
+HB.lock
+Definition subset (T : finType) (A B : mem_pred T) : bool := pred0b (predD A B).
+Canonical subset_unlock := Unlockable subset.unlock.
+
+Notation "A \subset B" := (subset (mem A) (mem B))
+  (at level 70, no associativity) : bool_scope.
+
+Definition proper T A B := @subset T A B && ~~ subset B A.
+Notation "A \proper B" := (proper (mem A) (mem B))
+  (at level 70, no associativity) : bool_scope.
+
+ 
+
+Section OpsTheory.
+
+Variable T : finType.
+
+Implicit Types (A B C D : {pred T}) (P Q : pred T) (x y : T) (s : seq T).
+
+Lemma enumP : Finite.axiom (Finite.enum T).
+Proof.
+by rewrite unlock; apply: enumP_subdef.
+Qed.
+
+Section EnumPick.
+
+Variable P : pred T.
+
+Lemma enumT : enum T = Finite.enum T.
+Proof.
+exact: filter_predT.
+Qed.
+
+Lemma mem_enum A : enum A =i A.
+Proof.
+by move=> x; rewrite mem_filter andbC -has_pred1 has_count enumP.
+Qed.
+
+Lemma enum_uniq A : uniq (enum A).
+Proof.
+by apply/filter_uniq/count_mem_uniq => x; rewrite enumP -enumT mem_enum.
+Qed.
+
+Lemma enum0 : enum pred0 = Nil T.
+Proof.
+exact: filter_pred0.
+Qed.
+
+Lemma enum1 x : enum (pred1 x) = [:: x].
+Proof.
+rewrite [enum _](all_pred1P x _ _); first by rewrite size_filter enumP.
+by apply/allP=> y; rewrite mem_enum.
+Qed.
+
+Variant pick_spec : option T -> Type :=
+  | Pick x of P x         : pick_spec (Some x)
+  | Nopick of P =1 xpred0 : pick_spec None.
+
+Lemma pickP : pick_spec (pick P).
+Proof.
+rewrite /pick; case: (enum _) (mem_enum P) => [|x s] Pxs /=.
+  by right; apply: fsym.
+by left; rewrite -[P _]Pxs mem_head.
+Qed.
+
+End EnumPick.
+
+Lemma eq_enum A B : A =i B -> enum A = enum B.
+Proof.
+by move=> eqAB; apply: eq_filter.
+Qed.
+
+Lemma eq_pick P Q : P =1 Q -> pick P = pick Q.
+Proof.
+by move=> eqPQ; rewrite /pick (eq_enum eqPQ).
+Qed.
+
+Lemma cardE A : #|A| = size (enum A).
+Proof.
+by rewrite unlock.
+Qed.
+
+Lemma eq_card A B : A =i B -> #|A| = #|B|.
+Proof.
+by move=> eqAB; rewrite !cardE (eq_enum eqAB).
+Qed.
+
+Lemma eq_card_trans A B n : #|A| = n -> B =i A -> #|B| = n.
+Proof.
+by move <-; apply: eq_card.
+Qed.
+
+Lemma card0 : #|@pred0 T| = 0.
+Proof.
+by rewrite cardE enum0.
+Qed.
+
+Lemma cardT : #|T| = size (enum T).
+Proof.
+by rewrite cardE.
+Qed.
+
+Lemma card1 x : #|pred1 x| = 1.
+Proof.
+by rewrite cardE enum1.
+Qed.
+
+Lemma eq_card0 A : A =i pred0 -> #|A| = 0.
+Proof.
+exact: eq_card_trans card0.
+Qed.
+
+Lemma eq_cardT A : A =i predT -> #|A| = size (enum T).
+Proof.
+exact: eq_card_trans cardT.
+Qed.
+
+Lemma eq_card1 x A : A =i pred1 x -> #|A| = 1.
+Proof.
+exact: eq_card_trans (card1 x).
+Qed.
+
+Lemma cardUI A B : #|[predU A & B]| + #|[predI A & B]| = #|A| + #|B|.
+Proof.
+by rewrite !cardE !size_filter count_predUI.
+Qed.
+
+Lemma cardID B A : #|[predI A & B]| + #|[predD A & B]| = #|A|.
+Proof.
+rewrite -cardUI addnC [#|predI _ _|]eq_card0 => [|x] /=.
+  by apply: eq_card => x; rewrite !inE andbC -andb_orl orbN.
+by rewrite !inE -!andbA andbC andbA andbN.
+Qed.
+
+Lemma cardC A : #|A| + #|[predC A]| = #|T|.
+Proof.
+by rewrite !cardE !size_filter count_predC.
+Qed.
+
+Lemma cardU1 x A : #|[predU1 x & A]| = (x \notin A) + #|A|.
+Proof.
+case Ax: (x \in A).
+  by apply: eq_card => y /[1!inE]/=; case: eqP => // ->.
+rewrite /= -(card1 x) -cardUI addnC.
+rewrite [#|predI _ _|]eq_card0 => [|y /=]; first exact: eq_card.
+by rewrite !inE; case: eqP => // ->.
+Qed.
+
+Lemma card2 x y : #|pred2 x y| = (x != y).+1.
+Proof.
+by rewrite cardU1 card1 addn1.
+Qed.
+
+Lemma cardC1 x : #|predC1 x| = #|T|.-1.
+Proof.
+by rewrite -(cardC (pred1 x)) card1.
+Qed.
+
+Lemma cardD1 x A : #|A| = (x \in A) + #|[predD1 A & x]|.
+Proof.
+case Ax: (x \in A); last first.
+  by apply: eq_card => y /[!inE]/=; case: eqP => // ->.
+rewrite /= -(card1 x) -cardUI addnC /=.
+rewrite [#|predI _ _|]eq_card0 => [|y]; last by rewrite !inE; case: eqP.
+by apply: eq_card => y /[!inE]; case: eqP => // ->.
+Qed.
+
+Lemma max_card A : #|A| <= #|T|.
+Proof.
+by rewrite -(cardC A) leq_addr.
+Qed.
+
+Lemma card_size s : #|s| <= size s.
+Proof.
+elim: s => [|x s IHs] /=; first by rewrite card0.
+by rewrite cardU1 /=; case: (~~ _) => //; apply: leqW.
+Qed.
+
+Lemma card_uniqP s : reflect (#|s| = size s) (uniq s).
+Proof.
+elim: s => [|x s IHs]; first by left; apply: card0.
+rewrite cardU1 /= /addn; case: {+}(x \in s) => /=.
+  by right=> card_Ssz; have:= card_size s; rewrite card_Ssz ltnn.
+by apply: (iffP IHs) => [<-| [<-]].
+Qed.
+
+Lemma card0_eq A : #|A| = 0 -> A =i pred0.
+Proof.
+by move=> A0 x; apply/idP => Ax; rewrite (cardD1 x) Ax in A0.
+Qed.
+
+Lemma fintype0 : T -> #|T| <> 0.
+Proof.
+by move=> x /card0_eq/(_ x).
+Qed.
+
+Lemma pred0P P : reflect (P =1 pred0) (pred0b P).
+Proof.
+by apply: (iffP eqP); [apply: card0_eq | apply: eq_card0].
+Qed.
+
+Lemma pred0Pn P : reflect (exists x, P x) (~~ pred0b P).
+Proof.
+case: (pickP P) => [x Px | P0].
+  by rewrite (introN (pred0P P)) => [|P0]; [left; exists x | rewrite P0 in Px].
+by rewrite -lt0n eq_card0 //; right=> [[x]]; rewrite P0.
+Qed.
+
+Lemma card_gt0P A : reflect (exists i, i \in A) (#|A| > 0).
+Proof.
+by rewrite lt0n; apply: pred0Pn.
+Qed.
+
+Lemma card_le1P {A} : reflect {in A, forall x, A =i pred1 x} (#|A| <= 1).
+Proof.
+apply: (iffP idP) => [A1 x xA y|]; last first.
+  by have [/= x xA /(_ _ xA)/eq_card1->|/eq_card0->//] := pickP [in A].
+move: A1; rewrite (cardD1 x) xA ltnS leqn0 => /eqP/card0_eq/(_ y).
+by rewrite !inE; have [->|]:= eqP.
+Qed.
+
+Lemma mem_card1 A : #|A| = 1 -> {x | A =i pred1 x}.
+Proof.
+move=> A1; have /card_gt0P/sigW[x xA]: #|A| > 0 by rewrite A1.
+by exists x; apply/card_le1P; rewrite ?A1.
+Qed.
+
+Lemma card1P A : reflect (exists x, A =i pred1 x) (#|A| == 1).
+Proof.
+by apply: (iffP idP) => [/eqP/mem_card1[x inA]|[x /eq_card1/eqP//]]; exists x.
+Qed.
+
+Lemma card_le1_eqP A :
+  reflect {in A &, forall x, all_equal_to x} (#|A| <= 1).
+Proof.
+apply: (iffP card_le1P) => [Ale1 x y xA yA /=|all_eq x xA y].
+  by apply/eqP; rewrite -[_ == _]/(y \in pred1 x) -Ale1.
+by rewrite inE; case: (altP (y =P x)) => [->//|]; exact/contra_neqF/all_eq.
+Qed.
+
+Lemma fintype_le1P : reflect (forall x : T, all_equal_to x) (#|T| <= 1).
+Proof.
+apply: (iffP (card_le1_eqP {:T})); [exact: in2T | exact: in2W].
+Qed.
+
+Lemma fintype1 : #|T| = 1 -> {x : T | all_equal_to x}.
+Proof.
+by move=> /mem_card1[x ex]; exists x => y; suff: y \in T by rewrite ex => /eqP.
+Qed.
+
+Lemma fintype1P : reflect (exists x, all_equal_to x) (#|T| == 1).
+Proof.
+apply: (iffP idP) => [/eqP/fintype1|] [x eqx]; first by exists x.
+by apply/card1P; exists x => y; rewrite eqx !inE eqxx.
+Qed.
+
+Lemma subsetE A B : (A \subset B) = pred0b [predD A & B].
+Proof.
+by rewrite unlock.
+Qed.
+
+Lemma subsetP A B : reflect {subset A <= B} (A \subset B).
+Proof.
+rewrite unlock; apply: (iffP (pred0P _)) => [AB0 x | sAB x /=].
+  by apply/implyP; apply/idPn; rewrite negb_imply andbC [_ && _]AB0.
+by rewrite andbC -negb_imply; apply/negbF/implyP; apply: sAB.
+Qed.
+
+Lemma subsetPn A B :
+  reflect (exists2 x, x \in A & x \notin B) (~~ (A \subset B)).
+Proof.
+rewrite unlock; apply: (iffP (pred0Pn _)) => [[x] | [x Ax nBx]].
+  by case/andP; exists x.
+by exists x; rewrite /= nBx.
+Qed.
+
+Lemma subset_leq_card A B : A \subset B -> #|A| <= #|B|.
+Proof.
+move=> sAB.
+rewrite -(cardID A B) [#|predI _ _|](@eq_card _ A) ?leq_addr //= => x.
+by rewrite !inE andbC; case Ax: (x \in A) => //; apply: subsetP Ax.
+Qed.
+
+Lemma subxx_hint (mA : mem_pred T) : subset mA mA.
+Proof.
+by case: mA => A; have:= introT (subsetP A A); rewrite !unlock => ->.
+Qed.
+Hint Resolve subxx_hint : core.
+
+ 
+Lemma subxx (pT : predType T) (pA : pT) : pA \subset pA.
+Proof.
+by [].
+Qed.
+
+Lemma eq_subset A B : A =i B -> subset (mem A) =1 subset (mem B).
+Proof.
+move=> eqAB [C]; rewrite !unlock; congr (_ == 0).
+by apply: eq_card => x; rewrite inE /= eqAB.
+Qed.
+
+Lemma eq_subset_r A B :
+   A =i B -> (@subset T)^~ (mem A) =1 (@subset T)^~ (mem B).
+Proof.
+move=> eqAB [C]; rewrite !unlock; congr (_ == 0).
+by apply: eq_card => x; rewrite !inE /= eqAB.
+Qed.
+
+Lemma eq_subxx A B : A =i B -> A \subset B.
+Proof.
+by move/eq_subset->.
+Qed.
+
+Lemma subset_predT A : A \subset T.
+Proof.
+exact/subsetP.
+Qed.
+
+Lemma predT_subset A : T \subset A -> forall x, x \in A.
+Proof.
+by move/subsetP=> allA x; apply: allA.
+Qed.
+
+Lemma subset_pred1 A x : (pred1 x \subset A) = (x \in A).
+Proof.
+by apply/subsetP/idP=> [-> // | Ax y /eqP-> //]; apply: eqxx.
+Qed.
+
+Lemma subset_eqP A B : reflect (A =i B) ((A \subset B) && (B \subset A)).
+Admitted.
+
+Lemma subset_cardP A B : #|A| = #|B| -> reflect (A =i B) (A \subset B).
+Admitted.
+
+Lemma subset_leqif_card A B : A \subset B -> #|A| <= #|B| ?= iff (B \subset A).
+Admitted.
+
+Lemma subset_trans A B C : A \subset B -> B \subset C -> A \subset C.
+Admitted.
+
+Lemma subset_all s A : (s \subset A) = all [in A] s.
+Admitted.
+
+Lemma subset_cons s x : s \subset x :: s.
+Admitted.
+
+Lemma subset_cons2 s1 s2 x : s1 \subset s2 -> x :: s1 \subset x :: s2.
+Admitted.
+
+Lemma subset_catl s s' : s \subset s ++ s'.
+Admitted.
+
+Lemma subset_catr s s' : s \subset s' ++ s.
+Admitted.
+
+Lemma subset_cat2 s1 s2 s3 : s1 \subset s2 -> s3 ++ s1 \subset s3 ++ s2.
+Admitted.
+
+Lemma filter_subset p s : [seq a <- s | p a] \subset s.
+Admitted.
+
+Lemma subset_filter p s1 s2 :
+  s1 \subset s2 -> [seq a <- s1 | p a] \subset [seq a <- s2 | p a].
+Admitted.
+
+Lemma properE A B : A \proper B = (A \subset B) && ~~ (B \subset A).
+Admitted.
+
+Lemma properP A B :
+  reflect (A \subset B /\ (exists2 x, x \in B & x \notin A)) (A \proper B).
+Admitted.
+
+Lemma proper_sub A B : A \proper B -> A \subset B.
+Admitted.
+
+Lemma proper_subn A B : A \proper B -> ~~ (B \subset A).
+Admitted.
+
+Lemma proper_trans A B C : A \proper B -> B \proper C -> A \proper C.
+Admitted.
+
+Lemma proper_sub_trans A B C : A \proper B -> B \subset C -> A \proper C.
+Admitted.
+
+Lemma sub_proper_trans A B C : A \subset B -> B \proper C -> A \proper C.
+Admitted.
+
+Lemma proper_card A B : A \proper B -> #|A| < #|B|.
+Admitted.
+
+Lemma proper_irrefl A : ~~ (A \proper A).
+Admitted.
+
+Lemma properxx A : (A \proper A) = false.
+Admitted.
+
+Lemma eq_proper A B : A =i B -> proper (mem A) =1 proper (mem B).
+Admitted.
+
+Lemma eq_proper_r A B :
+  A =i B -> (@proper T)^~ (mem A) =1 (@proper T)^~ (mem B).
+Admitted.
+
+Lemma card_geqP {A n} :
+  reflect (exists s, [/\ uniq s, size s = n & {subset s <= A}]) (n <= #|A|).
+Admitted.
+
+Lemma card_gt1P A :
+  reflect (exists x y, [/\ x \in A, y \in A & x != y]) (1 < #|A|).
+Admitted.
+
+Lemma card_gt2P A :
+  reflect (exists x y z,
+              [/\ x \in A, y \in A & z \in A] /\ [/\ x != y, y != z & z != x])
+          (2 < #|A|).
+Admitted.
+
+Lemma disjoint_sym A B : [disjoint A & B] = [disjoint B & A].
+Admitted.
+
+Lemma eq_disjoint A B : A =i B -> disjoint (mem A) =1 disjoint (mem B).
+Admitted.
+
+Lemma eq_disjoint_r A B : A =i B ->
+  (@disjoint T)^~ (mem A) =1 (@disjoint T)^~ (mem B).
+Admitted.
+
+Lemma subset_disjoint A B : (A \subset B) = [disjoint A & [predC B]].
+Admitted.
+
+Lemma disjoint_subset A B : [disjoint A & B] = (A \subset [predC B]).
+Admitted.
+
+Lemma disjointFr A B x : [disjoint A & B] -> x \in A -> x \in B = false.
+Admitted.
+
+Lemma disjointFl A B x : [disjoint A & B] -> x \in B -> x \in A = false.
+Admitted.
+
+Lemma disjointWl A B C :
+   A \subset B -> [disjoint B & C] -> [disjoint A & C].
+Admitted.
+
+Lemma disjointWr A B C : A \subset B -> [disjoint C & B] -> [disjoint C & A].
+Admitted.
+
+Lemma disjointW A B C D :
+  A \subset B -> C \subset D -> [disjoint B & D] -> [disjoint A & C].
+Admitted.
+
+Lemma disjoint0 A : [disjoint pred0 & A].
+Admitted.
+
+Lemma eq_disjoint0 A B : A =i pred0 -> [disjoint A & B].
+Admitted.
+
+Lemma disjoint1 x A : [disjoint pred1 x & A] = (x \notin A).
+Admitted.
+
+Lemma eq_disjoint1 x A B :
+  A =i pred1 x ->  [disjoint A & B] = (x \notin B).
+Admitted.
+
+Lemma disjointU A B C :
+  [disjoint predU A B & C] = [disjoint A & C] && [disjoint B & C].
+Admitted.
+
+Lemma disjointU1 x A B :
+  [disjoint predU1 x A & B] = (x \notin B) && [disjoint A & B].
+Admitted.
+
+Lemma disjoint_cons x s B :
+  [disjoint x :: s & B] = (x \notin B) && [disjoint s & B].
+Admitted.
+
+Lemma disjoint_has s A : [disjoint s & A] = ~~ has [in A] s.
+Admitted.
+
+Lemma disjoint_cat s1 s2 A :
+  [disjoint s1 ++ s2 & A] = [disjoint s1 & A] && [disjoint s2 & A].
+Admitted.
+
+End OpsTheory.
+
+Lemma map_subset {T T' : finType} (s1 s2 : seq T) (f : T -> T') :
+  s1 \subset s2 -> [seq f x | x <- s1 ] \subset [seq f x | x <- s2].
+Admitted.
+
+#[global] Hint Resolve subxx_hint : core.
+
+Arguments pred0P {T P}.
+Arguments pred0Pn {T P}.
+Arguments card_le1P {T A}.
+Arguments card_le1_eqP {T A}.
+Arguments card1P {T A}.
+Arguments fintype_le1P {T}.
+Arguments fintype1P {T}.
+Arguments subsetP {T A B}.
+Arguments subsetPn {T A B}.
+Arguments subset_eqP {T A B}.
+Arguments card_uniqP {T s}.
+Arguments card_geqP {T A n}.
+Arguments card_gt0P {T A}.
+Arguments card_gt1P {T A}.
+Arguments card_gt2P {T A}.
+Arguments properP {T A B}.
+
+ 
+ 
+ 
+ 
+ 
+
+Section QuantifierCombinators.
+
+Variables (T : finType) (P : pred T) (PP : T -> Prop).
+Hypothesis viewP : forall x, reflect (PP x) (P x).
+
+Lemma existsPP : reflect (exists x, PP x) [exists x, P x].
+Admitted.
+
+Lemma forallPP : reflect (forall x, PP x) [forall x, P x].
+Admitted.
+
+End QuantifierCombinators.
+
+Notation "'exists_ view" := (existsPP (fun _ => view))
+  (at level 4, right associativity, format "''exists_' view").
+Notation "'forall_ view" := (forallPP (fun _ => view))
+  (at level 4, right associativity, format "''forall_' view").
+
+Section Quantifiers.
+
+Variables (T : finType) (rT : T -> eqType).
+Implicit Types (D P : pred T) (f : forall x, rT x).
+
+Lemma forallP P : reflect (forall x, P x) [forall x, P x].
+Proof.
+exact: 'forall_idP.
+Qed.
+
+Lemma eqfunP f1 f2 : reflect (forall x, f1 x = f2 x) [forall x, f1 x == f2 x].
+Admitted.
+
+Lemma forall_inP D P : reflect (forall x, D x -> P x) [forall (x | D x), P x].
+Proof.
+exact: 'forall_implyP.
+Qed.
+
+Lemma forall_inPP D P PP : (forall x, reflect (PP x) (P x)) ->
+  reflect (forall x, D x -> PP x) [forall (x | D x), P x].
+Admitted.
+
+Lemma eqfun_inP D f1 f2 :
+  reflect {in D, forall x, f1 x = f2 x} [forall (x | x \in D), f1 x == f2 x].
+Admitted.
+
+Lemma existsP P : reflect (exists x, P x) [exists x, P x].
+Proof.
+exact: 'exists_idP.
+Qed.
+
+Lemma existsb P (x : T) : P x -> [exists x, P x].
+Proof.
+by move=> Px; apply/existsP; exists x.
+Qed.
+
+Lemma exists_eqP f1 f2 :
+  reflect (exists x, f1 x = f2 x) [exists x, f1 x == f2 x].
+Admitted.
+
+Lemma exists_inP D P : reflect (exists2 x, D x & P x) [exists (x | D x), P x].
+Proof.
+by apply: (iffP 'exists_andP) => [[x []] | [x]]; exists x.
+Qed.
+
+Lemma exists_inb D P (x : T) : D x -> P x -> [exists (x | D x), P x].
+Proof.
+by move=> Dx Px; apply/exists_inP; exists x.
+Qed.
+
+Lemma exists_inPP D P PP : (forall x, reflect (PP x) (P x)) ->
+  reflect (exists2 x, D x & PP x) [exists (x | D x), P x].
+Admitted.
+
+Lemma exists_eq_inP D f1 f2 :
+  reflect (exists2 x, D x & f1 x = f2 x) [exists (x | D x), f1 x == f2 x].
+Admitted.
+
+Lemma eq_existsb P1 P2 : P1 =1 P2 -> [exists x, P1 x] = [exists x, P2 x].
+Proof.
+by move=> eqP12; congr (_ != 0); apply: eq_card.
+Qed.
+
+Lemma eq_existsb_in D P1 P2 :
+    (forall x, D x -> P1 x = P2 x) ->
+  [exists (x | D x), P1 x] = [exists (x | D x), P2 x].
+Admitted.
+
+Lemma eq_forallb P1 P2 : P1 =1 P2 -> [forall x, P1 x] = [forall x, P2 x].
+Proof.
+by move=> eqP12; apply/negb_inj/eq_existsb=> /= x; rewrite eqP12.
+Qed.
+
+Lemma eq_forallb_in D P1 P2 :
+    (forall x, D x -> P1 x = P2 x) ->
+  [forall (x | D x), P1 x] = [forall (x | D x), P2 x].
+Admitted.
+
+Lemma negb_forall P : ~~ [forall x, P x] = [exists x, ~~ P x].
+Proof.
+by [].
+Qed.
+
+Lemma negb_forall_in D P :
+  ~~ [forall (x | D x), P x] = [exists (x | D x), ~~ P x].
+Proof.
+by apply: eq_existsb => x; rewrite negb_imply.
+Qed.
+
+Lemma negb_exists P : ~~ [exists x, P x] = [forall x, ~~ P x].
+Proof.
+by apply/negbLR/esym/eq_existsb=> x; apply: negbK.
+Qed.
+
+Lemma negb_exists_in D P :
+  ~~ [exists (x | D x), P x] = [forall (x | D x), ~~ P x].
+Proof.
+by rewrite negb_exists; apply/eq_forallb => x; rewrite [~~ _]fun_if.
+Qed.
+
+Lemma existsPn P :
+  reflect (forall x, ~~ P x) (~~ [exists x, P x]).
+Proof.
+rewrite negb_exists.
+exact: forallP.
+Qed.
+
+Lemma forallPn P :
+  reflect (exists x, ~~ P x) (~~ [forall x, P x]).
+Proof.
+rewrite negb_forall.
+exact: existsP.
+Qed.
+
+Lemma exists_inPn D P :
+  reflect (forall x, x \in D -> ~~ P x) (~~ [exists x in D, P x]).
+Proof.
+rewrite negb_exists_in.
+exact: forall_inP.
+Qed.
+
+Lemma forall_inPn D P :
+  reflect (exists2 x, x \in D & ~~ P x) (~~ [forall x in D, P x]).
+Proof.
+rewrite negb_forall_in.
+exact: exists_inP.
+Qed.
+
+End Quantifiers.
+
+Arguments forallP {T P}.
+Arguments eqfunP {T rT f1 f2}.
+Arguments forall_inP {T D P}.
+Arguments eqfun_inP {T rT D f1 f2}.
+Arguments existsP {T P}.
+Arguments existsb {T P}.
+Arguments exists_eqP {T rT f1 f2}.
+Arguments exists_inP {T D P}.
+Arguments exists_inb {T D P}.
+Arguments exists_eq_inP {T rT D f1 f2}.
+Arguments existsPn {T P}.
+Arguments exists_inPn {T D P}.
+Arguments forallPn {T P}.
+Arguments forall_inPn {T D P}.
+
+Notation "'exists_in_ view" := (exists_inPP _ (fun _ => view))
+  (at level 4, right associativity, format "''exists_in_' view").
+Notation "'forall_in_ view" := (forall_inPP _ (fun _ => view))
+  (at level 4, right associativity, format "''forall_in_' view").
+
+ 
+ 
+ 
+ 
+ 
+
+Section Injectiveb.
+
+Variables (aT : finType) (rT : eqType) (f : aT -> rT).
+Implicit Type D : {pred aT}.
+
+Definition dinjectiveb D := uniq (map f (enum D)).
+
+Definition injectiveb := dinjectiveb aT.
+
+Lemma dinjectivePn D :
+  reflect (exists2 x, x \in D & exists2 y, y \in [predD1 D & x] & f x = f y)
+          (~~ dinjectiveb D).
+Admitted.
+
+Lemma dinjectiveP D : reflect {in D &, injective f} (dinjectiveb D).
+Admitted.
+
+Lemma injectivePn :
+  reflect (exists x, exists2 y, x != y & f x = f y) (~~ injectiveb).
+Admitted.
+
+Lemma injectiveP : reflect (injective f) injectiveb.
+Admitted.
+
+End Injectiveb.
+
+Definition image_mem T T' f mA : seq T' := map f (@enum_mem T mA).
+Notation image f A := (image_mem f (mem A)).
+Notation "[ 'seq' F | x 'in' A ]" := (image (fun x => F) A)
+  (at level 0, F at level 99, x binder,
+   format "'[hv' [ 'seq'  F '/ '  |  x  'in'  A ] ']'") : seq_scope.
+Notation "[ 'seq' F | x ]" :=
+  [seq F | x in pred_of_simpl (@pred_of_argType
+     
+    match _, (fun x => I) with
+    | T, f
+      => match match f return T -> True with f' => f' end with
+         | _ => T
+         end
+    end)]
+  (at level 0, F at level 99, x binder, only parsing) : seq_scope.
+Notation "[ 'seq' F | x : T ]" :=
+  [seq F | x : T in pred_of_simpl (@pred_of_argType T)]
+  (at level 0, F at level 99, x name, only printing,
+   format "'[hv' [ 'seq'  F '/ '  |  x  :  T ] ']'") : seq_scope.
+Notation "[ 'seq' F , x ]" := [seq F | x ]
+  (at level 0, F at level 99, x binder, only parsing) : seq_scope.
+
+Definition codom T T' f := @image_mem T T' f (mem T).
+
+Section Image.
+
+Variable T : finType.
+Implicit Type A : {pred T}.
+
+Section SizeImage.
+
+Variables (T' : Type) (f : T -> T').
+
+Lemma size_image A : size (image f A) = #|A|.
+Admitted.
+
+Lemma size_codom : size (codom f) = #|T|.
+Admitted.
+
+Lemma codomE : codom f = map f (enum T).
+Admitted.
+
+End SizeImage.
+
+Variables (T' : eqType) (f : T -> T').
+
+Lemma imageP A y : reflect (exists2 x, x \in A & y = f x) (y \in image f A).
+Admitted.
+
+Lemma codomP y : reflect (exists x, y = f x) (y \in codom f).
+Admitted.
+
+Remark iinv_proof A y : y \in image f A -> {x | x \in A & f x = y}.
+Admitted.
+
+Definition iinv A y fAy := s2val (@iinv_proof A y fAy).
+
+Lemma f_iinv A y fAy : f (@iinv A y fAy) = y.
+Admitted.
+
+Lemma mem_iinv A y fAy : @iinv A y fAy \in A.
+Admitted.
+
+Lemma in_iinv_f A : {in A &, injective f} ->
+  forall x fAfx, x \in A -> @iinv A (f x) fAfx = x.
+Admitted.
+
+Lemma preim_iinv A B y fAy : preim f B (@iinv A y fAy) = B y.
+Admitted.
+
+Lemma image_f A x : x \in A -> f x \in image f A.
+Admitted.
+
+Lemma codom_f x : f x \in codom f.
+Admitted.
+
+Lemma image_codom A : {subset image f A <= codom f}.
+Admitted.
+
+Lemma image_pred0 : image f pred0 =i pred0.
+Admitted.
+
+Section Injective.
+
+Hypothesis injf : injective f.
+
+Lemma mem_image A x : (f x \in image f A) = (x \in A).
+Admitted.
+
+Lemma pre_image A : [preim f of image f A] =i A.
+Admitted.
+
+Lemma image_iinv A y (fTy : y \in codom f) :
+  (y \in image f A) = (iinv fTy \in A).
+Admitted.
+
+Lemma iinv_f x fTfx : @iinv T (f x) fTfx = x.
+Admitted.
+
+Lemma image_pre (B : pred T') : image f [preim f of B] =i [predI B & codom f].
+Admitted.
+
+Lemma bij_on_codom (x0 : T) : {on [pred y in codom f], bijective f}.
+Admitted.
+
+Lemma bij_on_image A (x0 : T) : {on [pred y in image f A], bijective f}.
+Admitted.
+
+End Injective.
+
+Fixpoint preim_seq s :=
+  if s is y :: s' then
+    (if pick (preim f (pred1 y)) is Some x then cons x else id) (preim_seq s')
+    else [::].
+
+Lemma map_preim (s : seq T') : {subset s <= codom f} -> map f (preim_seq s) = s.
+Admitted.
+
+End Image.
+
+Prenex Implicits codom iinv.
+Arguments imageP {T T' f A y}.
+Arguments codomP {T T' f y}.
+
+Lemma flatten_imageP (aT : finType) (rT : eqType)
+                     (A : aT -> seq rT) (P : {pred aT}) (y : rT) :
+  reflect (exists2 x, x \in P & y \in A x) (y \in flatten [seq A x | x in P]).
+Admitted.
+Arguments flatten_imageP {aT rT A P y}.
+
+Section CardFunImage.
+
+Variables (T T' : finType) (f : T -> T').
+Implicit Type A : {pred T}.
+
+Lemma leq_image_card A : #|image f A| <= #|A|.
+Admitted.
+
+Lemma card_in_image A : {in A &, injective f} -> #|image f A| = #|A|.
+Admitted.
+
+Lemma image_injP A : reflect {in A &, injective f} (#|image f A| == #|A|).
+Admitted.
+
+Lemma leq_card_in A : {in A &, injective f} -> #|A| <= #|T'|.
+Admitted.
+
+Hypothesis injf : injective f.
+
+Lemma card_image A : #|image f A| = #|A|.
+Admitted.
+
+Lemma card_codom : #|codom f| = #|T|.
+Admitted.
+
+Lemma card_preim (B : {pred T'}) : #|[preim f of B]| = #|[predI codom f & B]|.
+Admitted.
+
+Lemma leq_card : #|T| <= #|T'|.
+Admitted.
+
+Hypothesis card_range : #|T| >= #|T'|.
+
+Let eq_card : #|T| = #|T'|.
+Proof.
+by apply/eqP; rewrite eqn_leq leq_card.
+Qed.
+
+Lemma inj_card_onto y : y \in codom f.
+Admitted.
+
+Lemma inj_card_bij :  bijective f.
+Admitted.
+
+End CardFunImage.
+
+Arguments image_injP {T T' f A}.
+Arguments leq_card_in [T T'] f.
+Arguments leq_card [T T'] f.
+
+Lemma bij_eq_card (T T' : finType) (f : T -> T') : bijective f -> #|T| = #|T'|.
+Admitted.
+
+Section FinCancel.
+
+Variables (T : finType) (f g : T -> T).
+
+Section Inv.
+
+Hypothesis injf : injective f.
+
+Lemma injF_onto y : y \in codom f.
+Proof.
+exact: inj_card_onto.
+Qed.
+Definition invF y := iinv (injF_onto y).
+Lemma invF_f : cancel f invF.
+Admitted.
+Lemma f_invF : cancel invF f.
+Admitted.
+Lemma injF_bij : bijective f.
+Admitted.
+
+End Inv.
+
+Hypothesis fK : cancel f g.
+
+Lemma canF_sym : cancel g f.
+Admitted.
+
+Lemma canF_LR x y : x = g y -> f x = y.
+Admitted.
+
+Lemma canF_RL x y : g x = y -> x = f y.
+Admitted.
+
+Lemma canF_eq x y : (f x == y) = (x == g y).
+Admitted.
+
+Lemma canF_invF : g =1 invF (can_inj fK).
+Admitted.
+
+End FinCancel.
+
+Section EqImage.
+
+Variables (T : finType) (T' : Type).
+
+Lemma eq_image (A B : {pred T}) (f g : T -> T') :
+  A =i B -> f =1 g -> image f A = image g B.
+Admitted.
+
+Lemma eq_codom (f g : T -> T') : f =1 g -> codom f = codom g.
+Admitted.
+
+Lemma eq_invF f g injf injg : f =1 g -> @invF T f injf =1 @invF T g injg.
+Admitted.
+
+End EqImage.
+
+ 
+
+Lemma unit_enumP : Finite.axiom [::tt].
+Admitted.
+HB.instance Definition _ := isFinite.Build unit unit_enumP.
+Lemma card_unit : #|{: unit}| = 1.
+Admitted.
+
+Lemma bool_enumP : Finite.axiom [:: true; false].
+Admitted.
+HB.instance Definition _ := isFinite.Build bool bool_enumP.
+Lemma card_bool : #|{: bool}| = 2.
+Admitted.
+
+Lemma void_enumP : Finite.axiom (Nil void).
+Admitted.
+HB.instance Definition _ := isFinite.Build void void_enumP.
+Lemma card_void : #|{: void}| = 0.
+Admitted.
+
+Local Notation enumF T := (Finite.enum T).
+
+Section OptionFinType.
+
+Variable T : finType.
+
+Definition option_enum := None :: map some (enumF T).
+
+Lemma option_enumP : Finite.axiom option_enum.
+Admitted.
+
+HB.instance Definition _ := isFinite.Build (option T) option_enumP.
+
+Lemma card_option : #|{: option T}| = #|T|.+1.
+Admitted.
+
+End OptionFinType.
+
+Section TransferFinTypeFromCount.
+
+Variables (eT : countType) (fT : finType) (f : eT -> fT).
+
+Lemma pcan_enumP g : pcancel f g -> Finite.axiom (undup (pmap g (enumF fT))).
+Admitted.
+
+Definition PCanIsFinite g fK := @isFinite.Build _ _ (@pcan_enumP g fK).
+
+Definition CanIsFinite g (fK : cancel f g) := PCanIsFinite (can_pcan fK).
+
+End TransferFinTypeFromCount.
+
+#[deprecated(since="mathcomp 2.0.0",
+  note="Use pcan_type instead or PCanIsFInite.")]
+Notation PcanFinMixin := PCanIsFinite.
+#[deprecated(since="mathcomp 2.0.0",
+  note="Use can_type instead or CanIsFinite.")]
+Notation CanFinMixin := CanIsFinite.
+
+Section TransferFinType.
+
+Variables (eT : Type) (fT : finType) (f : eT -> fT).
+
+HB.instance Definition _ (g : fT -> option eT) (fK : pcancel f g) :=
+  isFinite.Build (pcan_type fK) (@pcan_enumP (pcan_type fK) fT f g fK).
+
+HB.instance Definition _ (g : fT -> eT) (fK : cancel f g) :=
+  isFinite.Build (can_type fK) (@pcan_enumP (can_type fK) fT f _ (can_pcan fK)).
+
+End TransferFinType.
+
+#[short(type="subFinType")]
+HB.structure Definition SubFinite (T : Type) (P : pred T) :=
+  { sT of Finite sT & isSub T P sT }.
+
+Section SubFinType.
+
+Variables (T : choiceType) (P : pred T).
+Import Finite.
+
+Implicit Type sT : subFinType P.
+
+Lemma codom_val sT x : (x \in codom (val : sT -> T)) = P x.
+Admitted.
+
+End SubFinType.
+
+#[deprecated(since="mathcomp 2.0.0", note="Use SubFinite.clone instead.")]
+Notation "[ 'subFinType' 'of' T ]" := (SubFinite.clone _ _ T%type _)
+  (at level 0, format "[ 'subFinType'  'of'  T ]") : form_scope.
+
+HB.factory Record SubCountable_isFinite (T : finType) P (sT : Type)
+  of SubCountable T P sT := { }.
+
+HB.builders Context (T : finType) (P : pred T) (sT : Type)
+  (a : SubCountable_isFinite T P sT).
+
+Definition sub_enum : seq sT := pmap insub (enumF T).
+
+Lemma mem_sub_enum u : u \in sub_enum.
+Admitted.
+
+Lemma sub_enum_uniq : uniq sub_enum.
+Admitted.
+
+Lemma val_sub_enum : map val sub_enum = enum P.
+Admitted.
+
+HB.instance Definition SubFinMixin := isFinite.Build sT
+  (Finite.uniq_enumP sub_enum_uniq mem_sub_enum).
+HB.end.
+
+ 
+ 
+
+HB.instance Definition _ (T : finType) (P : pred T) (sT : subType P) :=
+  (SubCountable_isFinite.Build _ _ (sub_type sT)).
+
+Notation "[ 'Finite' 'of' T 'by' <: ]" := (Finite.copy T%type (sub_type T%type))
+  (at level 0, format "[ 'Finite'  'of'  T  'by'  <: ]") : form_scope.
+#[deprecated(since="mathcomp 2.0.0", note="Use [Finite of _ by <:] instead.")]
+Notation "[ 'finMixin' 'of' T 'by' <: ]" := [Finite of T%type by <:]
+  (at level 0, format "[ 'finMixin'  'of'  T  'by'  <: ]") : form_scope.
+
+Section SubCountable_isFiniteTheory.
+
+Variables (T : finType) (P : pred T) (sfT : subFinType P).
+
+Lemma card_sub : #|sfT| = #|[pred x | P x]|.
+Admitted.
+
+Lemma eq_card_sub (A : {pred sfT}) : A =i predT -> #|A| = #|[pred x | P x]|.
+Admitted.
+
+End SubCountable_isFiniteTheory.
+
+ 
+ 
+ 
+ 
+ 
+ 
+ 
+
+Section CardSig.
+
+Variables (T : finType) (P : pred T).
+
+HB.instance Definition _ := [Finite of {x | P x} by <:].
+
+Lemma card_sig : #|{: {x | P x}}| = #|[pred x | P x]|.
+Admitted.
+
+End CardSig.
+
+ 
+Section SeqSubType.
+
+Variables (T : eqType) (s : seq T).
+
+Record seq_sub : Type := SeqSub {ssval : T; ssvalP : in_mem ssval (@mem T _ s)}.
+
+HB.instance Definition _ := [isSub for ssval].
+HB.instance Definition _ := [Equality of seq_sub by <:].
+
+Definition seq_sub_enum : seq seq_sub := undup (pmap insub s).
+
+Lemma mem_seq_sub_enum x : x \in seq_sub_enum.
+Admitted.
+
+Lemma val_seq_sub_enum : uniq s -> map val seq_sub_enum = s.
+Admitted.
+
+Definition seq_sub_pickle x := index x seq_sub_enum.
+Definition seq_sub_unpickle n := nth None (map some seq_sub_enum) n.
+Lemma seq_sub_pickleK : pcancel seq_sub_pickle seq_sub_unpickle.
+Admitted.
+
+Definition seq_sub_isCountable := isCountable.Build seq_sub seq_sub_pickleK.
+Fact seq_sub_axiom : Finite.axiom seq_sub_enum.
+Admitted.
+Definition seq_sub_isFinite := isFinite.Build seq_sub seq_sub_axiom.
+
+ 
+ 
+Definition adhoc_seq_sub_choiceType : choiceType := pcan_type seq_sub_pickleK.
+Definition adhoc_seq_sub_countType := HB.pack_for countType seq_sub
+  seq_sub_isCountable (Choice.class adhoc_seq_sub_choiceType).
+Definition adhoc_seq_sub_finType := HB.pack_for finType seq_sub
+  seq_sub_isFinite seq_sub_isCountable (Choice.class adhoc_seq_sub_choiceType).
+
+End SeqSubType.
+
+Section SeqReplace.
+Variables (T : eqType).
+Implicit Types (s : seq T).
+
+Lemma seq_sub_default s : size s > 0 -> seq_sub s.
+Admitted.
+
+Lemma seq_subE s (s_gt0 : size s > 0) :
+  s = map val (map (insubd (seq_sub_default s_gt0)) s : seq (seq_sub s)).
+Admitted.
+
+End SeqReplace.
+Notation in_sub_seq s_gt0 := (insubd (seq_sub_default s_gt0)).
+
+Section SeqFinType.
+
+Variables (T : choiceType) (s : seq T).
+Local Notation sT := (seq_sub s).
+
+HB.instance Definition _ := [Choice of sT by <:].
+HB.instance Definition _ : isCountable sT := seq_sub_isCountable s.
+HB.instance Definition _ : isFinite sT := seq_sub_isFinite s.
+
+Lemma card_seq_sub : uniq s -> #|{:sT}| = size s.
+Admitted.
+
+End SeqFinType.
+
+Section Extrema.
+
+Variant extremum_spec {T : eqType} (ord : rel T) {I : finType}
+  (P : pred I) (F : I -> T) : I -> Type :=
+  ExtremumSpec (i : I) of P i & (forall j : I, P j -> ord (F i) (F j)) :
+                   extremum_spec ord P F i.
+
+Let arg_pred {T : eqType} ord {I : finType} (P : pred I) (F : I -> T) :=
+  [pred i | P i & [forall (j | P j), ord (F i) (F j)]].
+
+Section Extremum.
+
+Context {T : eqType} {I : finType} (ord : rel T).
+Context (i0 : I) (P : pred I) (F : I -> T).
+
+Definition extremum := odflt i0 (pick (arg_pred ord P F)).
+
+Hypothesis ord_refl : reflexive ord.
+Hypothesis ord_trans : transitive ord.
+Hypothesis ord_total : total ord.
+Hypothesis Pi0 : P i0.
+
+Lemma extremumP : extremum_spec ord P F extremum.
+Admitted.
+
+End Extremum.
+
+Section ExtremumIn.
+
+Context {T : eqType} {I : finType} (ord : rel T).
+Context (i0 : I) (P : pred I) (F : I -> T).
+
+Hypothesis ord_refl : {in P, reflexive (relpre F ord)}.
+Hypothesis ord_trans : {in P & P & P, transitive (relpre F ord)}.
+Hypothesis ord_total : {in P &, total (relpre F ord)}.
+Hypothesis Pi0 : P i0.
+
+Lemma extremum_inP : extremum_spec ord P F (extremum ord i0 P F).
+Admitted.
+
+End ExtremumIn.
+
+Notation "[ 'arg[' ord ]_( i < i0 | P ) F ]" :=
+    (extremum ord i0 (fun i => P%B) (fun i => F))
+  (at level 0, ord, i, i0 at level 10,
+   format "[ 'arg[' ord ]_( i  <  i0  |  P )  F ]") : nat_scope.
+
+Notation "[ 'arg[' ord ]_( i < i0 'in' A ) F ]" :=
+    [arg[ord]_(i < i0 | i \in A) F]
+  (at level 0, ord, i, i0 at level 10,
+   format "[ 'arg[' ord ]_( i  <  i0  'in'  A )  F ]") : nat_scope.
+
+Notation "[ 'arg[' ord ]_( i < i0 ) F ]" := [arg[ord]_(i < i0 | true) F]
+  (at level 0, ord, i, i0 at level 10,
+   format "[ 'arg[' ord ]_( i  <  i0 )  F ]") : nat_scope.
+
+Section ArgMinMax.
+
+Variables (I : finType) (i0 : I) (P : pred I) (F : I -> nat) (Pi0 : P i0).
+
+Definition arg_min := extremum leq i0 P F.
+Definition arg_max := extremum geq i0 P F.
+
+Lemma arg_minnP : extremum_spec leq P F arg_min.
+Admitted.
+
+Lemma arg_maxnP : extremum_spec geq P F arg_max.
+Admitted.
+
+End ArgMinMax.
+
+End Extrema.
+
+Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" :=
+    (arg_min i0 (fun i => P%B) (fun i => F))
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg'  'min_' ( i  <  i0  |  P )  F ]") : nat_scope.
+
+Notation "[ 'arg' 'min_' ( i < i0 'in' A ) F ]" :=
+    [arg min_(i < i0 | i \in A) F]
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg'  'min_' ( i  <  i0  'in'  A )  F ]") : nat_scope.
+
+Notation "[ 'arg' 'min_' ( i < i0 ) F ]" := [arg min_(i < i0 | true) F]
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg'  'min_' ( i  <  i0 )  F ]") : nat_scope.
+
+Notation "[ 'arg' 'max_' ( i > i0 | P ) F ]" :=
+     (arg_max i0 (fun i => P%B) (fun i => F))
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg'  'max_' ( i  >  i0  |  P )  F ]") : nat_scope.
+
+Notation "[ 'arg' 'max_' ( i > i0 'in' A ) F ]" :=
+    [arg max_(i > i0 | i \in A) F]
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg'  'max_' ( i  >  i0  'in'  A )  F ]") : nat_scope.
+
+Notation "[ 'arg' 'max_' ( i > i0 ) F ]" := [arg max_(i > i0 | true) F]
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg'  'max_' ( i  >  i0 )  F ]") : nat_scope.
+
+ 
+ 
+ 
+ 
+ 
+
+Section OrdinalSub.
+
+Variable n : nat.
+
+Inductive ordinal : predArgType := Ordinal m of m < n.
+
+Coercion nat_of_ord i := let: Ordinal m _ := i in m.
+
+HB.instance Definition _ := [isSub of ordinal for nat_of_ord].
+HB.instance Definition _ := [Countable of ordinal by <:].
+
+Lemma ltn_ord (i : ordinal) : i < n.
+Admitted.
+
+Lemma ord_inj : injective nat_of_ord.
+Admitted.
+
+Definition ord_enum : seq ordinal := pmap insub (iota 0 n).
+
+Lemma val_ord_enum : map val ord_enum = iota 0 n.
+Admitted.
+
+Lemma ord_enum_uniq : uniq ord_enum.
+Admitted.
+
+Lemma mem_ord_enum i : i \in ord_enum.
+Admitted.
+
+HB.instance Definition _ := isFinite.Build ordinal
+  (Finite.uniq_enumP ord_enum_uniq mem_ord_enum).
+
+End OrdinalSub.
+
+Notation "''I_' n" := (ordinal n)
+  (at level 8, n at level 2, format "''I_' n").
+
+#[global] Hint Resolve ltn_ord : core.
+
+Section OrdinalEnum.
+
+Variable n : nat.
+
+Lemma val_enum_ord : map val (enum 'I_n) = iota 0 n.
+Admitted.
+
+Lemma size_enum_ord : size (enum 'I_n) = n.
+Admitted.
+
+Lemma card_ord : #|'I_n| = n.
+Admitted.
+
+Lemma nth_enum_ord i0 m : m < n -> nth i0 (enum 'I_n) m = m :> nat.
+Admitted.
+
+Lemma nth_ord_enum (i0 i : 'I_n) : nth i0 (enum 'I_n) i = i.
+Admitted.
+
+Lemma index_enum_ord (i : 'I_n) : index i (enum 'I_n) = i.
+Admitted.
+
+Lemma mask_enum_ord m :
+  mask m (enum 'I_n) = [seq i <- enum 'I_n | nth false m (val i)].
+Admitted.
+
+End OrdinalEnum.
+
+Lemma enum_ord0 : enum 'I_0 = [::].
+Admitted.
+
+Lemma widen_ord_proof n m (i : 'I_n) : n <= m -> i < m.
+Admitted.
+Definition widen_ord n m le_n_m i := Ordinal (@widen_ord_proof n m i le_n_m).
+
+Lemma cast_ord_proof n m (i : 'I_n) : n = m -> i < m.
+Admitted.
+Definition cast_ord n m eq_n_m i := Ordinal (@cast_ord_proof n m i eq_n_m).
+
+Lemma cast_ord_id n eq_n i : cast_ord eq_n i = i :> 'I_n.
+Admitted.
+
+Lemma cast_ord_comp n1 n2 n3 eq_n2 eq_n3 i :
+  @cast_ord n2 n3 eq_n3 (@cast_ord n1 n2 eq_n2 i) =
+    cast_ord (etrans eq_n2 eq_n3) i.
+Admitted.
+
+Lemma cast_ordK n1 n2 eq_n :
+  cancel (@cast_ord n1 n2 eq_n) (cast_ord (esym eq_n)).
+Admitted.
+
+Lemma cast_ordKV n1 n2 eq_n :
+  cancel (cast_ord (esym eq_n)) (@cast_ord n1 n2 eq_n).
+Admitted.
+
+Lemma cast_ord_inj n1 n2 eq_n : injective (@cast_ord n1 n2 eq_n).
+Admitted.
+
+Fact ordS_subproof n (i : 'I_n) : i.+1 %% n < n.
+Admitted.
+Definition ordS n (i : 'I_n) := Ordinal (ordS_subproof i).
+
+Fact ord_pred_subproof n (i : 'I_n) : (i + n).-1 %% n < n.
+Admitted.
+Definition ord_pred n (i : 'I_n) := Ordinal (ord_pred_subproof i).
+
+Lemma ordSK n : cancel (@ordS n) (@ord_pred n).
+Admitted.
+
+Lemma ord_predK n : cancel (@ord_pred n) (@ordS n).
+Admitted.
+
+Lemma ordS_bij n : bijective (@ordS n).
+Admitted.
+
+Lemma ordS_inj n : injective (@ordS n).
+Admitted.
+
+Lemma ord_pred_bij n : bijective (@ord_pred n).
+Admitted.
+
+Lemma ord_pred_inj n : injective (@ord_pred n).
+Admitted.
+
+Lemma rev_ord_proof n (i : 'I_n) : n - i.+1  < n.
+Admitted.
+Definition rev_ord n i := Ordinal (@rev_ord_proof n i).
+
+Lemma rev_ordK {n} : involutive (@rev_ord n).
+Admitted.
+
+Lemma rev_ord_inj {n} : injective (@rev_ord n).
+Admitted.
+
+Lemma inj_leq m n (f : 'I_m -> 'I_n) : injective f -> m <= n.
+Admitted.
+Arguments inj_leq [m n] f _.
+
+ 
+
+Lemma enum_rank_subproof (T : finType) x0 (A : {pred T}) : x0 \in A -> 0 < #|A|.
+Admitted.
+
+HB.lock
+Definition enum_rank_in (T : finType) x0 (A : {pred T}) (Ax0 : x0 \in A) x :=
+  insubd (Ordinal (@enum_rank_subproof T x0 [eta A] Ax0)) (index x (enum A)).
+Canonical unlockable_enum_rank_in := Unlockable enum_rank_in.unlock.
+
+Section EnumRank.
+
+Variable T : finType.
+Implicit Type A : {pred T}.
+
+Definition enum_rank x := @enum_rank_in T x T (erefl true) x.
+
+Lemma enum_default A : 'I_(#|A|) -> T.
+Admitted.
+
+Definition enum_val A i := nth (@enum_default [eta A] i) (enum A) i.
+Prenex Implicits enum_val.
+
+Lemma enum_valP A i : @enum_val A i \in A.
+Admitted.
+
+Lemma enum_val_nth A x i : @enum_val A i = nth x (enum A) i.
+Admitted.
+
+Lemma nth_image T' y0 (f : T -> T') A (i : 'I_#|A|) :
+  nth y0 (image f A) i = f (enum_val i).
+Admitted.
+
+Lemma nth_codom T' y0 (f : T -> T') (i : 'I_#|T|) :
+  nth y0 (codom f) i = f (enum_val i).
+Admitted.
+
+Lemma nth_enum_rank_in x00 x0 A Ax0 :
+  {in A, cancel (@enum_rank_in T x0 A Ax0) (nth x00 (enum A))}.
+Admitted.
+
+Lemma nth_enum_rank x0 : cancel enum_rank (nth x0 (enum T)).
+Admitted.
+
+Lemma enum_rankK_in x0 A Ax0 :
+   {in A, cancel (@enum_rank_in T x0 A Ax0) enum_val}.
+Admitted.
+
+Lemma enum_rankK : cancel enum_rank enum_val.
+Admitted.
+
+Lemma enum_valK_in x0 A Ax0 : cancel enum_val (@enum_rank_in T x0 A Ax0).
+Admitted.
+
+Lemma enum_valK : cancel enum_val enum_rank.
+Admitted.
+
+Lemma enum_rank_inj : injective enum_rank.
+Admitted.
+
+Lemma enum_val_inj A : injective (@enum_val A).
+Admitted.
+
+Lemma enum_val_bij_in x0 A : x0 \in A -> {on A, bijective (@enum_val A)}.
+Admitted.
+
+Lemma eq_enum_rank_in (x0 y0 : T) A (Ax0 : x0 \in A) (Ay0 : y0 \in A) :
+  {in A, enum_rank_in Ax0 =1 enum_rank_in Ay0}.
+Admitted.
+
+Lemma enum_rank_in_inj (x0 y0 : T) A (Ax0 : x0 \in A) (Ay0 : y0 \in A) :
+  {in A &, forall x y, enum_rank_in Ax0 x = enum_rank_in Ay0 y -> x = y}.
+Admitted.
+
+Lemma enum_rank_bij : bijective enum_rank.
+Admitted.
+
+Lemma enum_val_bij : bijective (@enum_val T).
+Admitted.
+
+ 
+ 
+ 
+Lemma fin_all_exists U (P : forall x : T, U x -> Prop) :
+  (forall x, exists u, P x u) -> (exists u, forall x, P x (u x)).
+Admitted.
+
+Lemma fin_all_exists2 U (P Q : forall x : T, U x -> Prop) :
+    (forall x, exists2 u, P x u & Q x u) ->
+  (exists2 u, forall x, P x (u x) & forall x, Q x (u x)).
+Admitted.
+
+End EnumRank.
+
+Arguments enum_val_inj {T A} [i1 i2] : rename.
+Arguments enum_rank_inj {T} [x1 x2].
+Prenex Implicits enum_val enum_rank enum_valK enum_rankK.
+
+Lemma enum_rank_ord n i : enum_rank i = cast_ord (esym (card_ord n)) i.
+Admitted.
+
+Lemma enum_val_ord n i : enum_val i = cast_ord (card_ord n) i.
+Admitted.
+
+ 
+
+Definition bump h i := (h <= i) + i.
+Definition unbump h i := i - (h < i).
+
+Lemma bumpK h : cancel (bump h) (unbump h).
+Admitted.
+
+Lemma neq_bump h i : h != bump h i.
+Admitted.
+
+Lemma unbumpKcond h i : bump h (unbump h i) = (i == h) + i.
+Admitted.
+
+Lemma unbumpK {h} : {in predC1 h, cancel (unbump h) (bump h)}.
+Admitted.
+
+Lemma bumpDl h i k : bump (k + h) (k + i) = k + bump h i.
+Admitted.
+
+Lemma bumpS h i : bump h.+1 i.+1 = (bump h i).+1.
+Admitted.
+
+Lemma unbumpDl h i k : unbump (k + h) (k + i) = k + unbump h i.
+Admitted.
+
+Lemma unbumpS h i : unbump h.+1 i.+1 = (unbump h i).+1.
+Admitted.
+
+Lemma leq_bump h i j : (i <= bump h j) = (unbump h i <= j).
+Admitted.
+
+Lemma leq_bump2 h i j : (bump h i <= bump h j) = (i <= j).
+Admitted.
+
+Lemma bumpC h1 h2 i :
+  bump h1 (bump h2 i) = bump (bump h1 h2) (bump (unbump h2 h1) i).
+Admitted.
+
+ 
+ 
+
+Lemma lift_subproof n h (i : 'I_n.-1) : bump h i < n.
+Admitted.
+
+Definition lift n (h : 'I_n) (i : 'I_n.-1) := Ordinal (lift_subproof h i).
+
+Lemma unlift_subproof n (h : 'I_n) (u : {j | j != h}) : unbump h (val u) < n.-1.
+Admitted.
+
+Definition unlift n (h i : 'I_n) :=
+  omap (fun u : {j | j != h} => Ordinal (unlift_subproof u)) (insub i).
+
+Variant unlift_spec n h i : option 'I_n.-1 -> Type :=
+  | UnliftSome j of i = lift h j : unlift_spec h i (Some j)
+  | UnliftNone   of i = h        : unlift_spec h i None.
+
+Lemma unliftP n (h i : 'I_n) : unlift_spec h i (unlift h i).
+Admitted.
+
+Lemma neq_lift n (h : 'I_n) i : h != lift h i.
+Admitted.
+
+Lemma eq_liftF n (h : 'I_n) i : (h == lift h i) = false.
+Admitted.
+
+Lemma lift_eqF n (h : 'I_n) i : (lift h i == h) = false.
+Admitted.
+
+Lemma unlift_none n (h : 'I_n) : unlift h h = None.
+Admitted.
+
+Lemma unlift_some n (h i : 'I_n) :
+  h != i -> {j | i = lift h j & unlift h i = Some j}.
+Admitted.
+
+Lemma lift_inj n (h : 'I_n) : injective (lift h).
+Admitted.
+Arguments lift_inj {n h} [i1 i2] eq_i12h : rename.
+
+Lemma liftK n (h : 'I_n) : pcancel (lift h) (unlift h).
+Admitted.
+
+ 
+
+Lemma lshift_subproof m n (i : 'I_m) : i < m + n.
+Admitted.
+
+Lemma rshift_subproof m n (i : 'I_n) : m + i < m + n.
+Admitted.
+
+Definition lshift m n (i : 'I_m) := Ordinal (lshift_subproof n i).
+Definition rshift m n (i : 'I_n) := Ordinal (rshift_subproof m i).
+
+Lemma lshift_inj m n : injective (@lshift m n).
+Admitted.
+
+Lemma rshift_inj m n : injective (@rshift m n).
+Admitted.
+
+Lemma eq_lshift m n i j : (@lshift m n i == @lshift m n j) = (i == j).
+Admitted.
+
+Lemma eq_rshift m n i j : (@rshift m n i == @rshift m n j) = (i == j).
+Admitted.
+
+Lemma eq_lrshift m n i j : (@lshift m n i == @rshift m n j) = false.
+Admitted.
+
+Lemma eq_rlshift m n i j : (@rshift m n i == @lshift m n j) = false.
+Admitted.
+
+Definition eq_shift := (eq_lshift, eq_rshift, eq_lrshift, eq_rlshift).
+
+Lemma split_subproof m n (i : 'I_(m + n)) : i >= m -> i - m < n.
+Admitted.
+
+Definition split {m n} (i : 'I_(m + n)) : 'I_m + 'I_n :=
+  match ltnP (i) m with
+  | LtnNotGeq lt_i_m =>  inl _ (Ordinal lt_i_m)
+  | GeqNotLtn ge_i_m =>  inr _ (Ordinal (split_subproof ge_i_m))
+  end.
+
+Variant split_spec m n (i : 'I_(m + n)) : 'I_m + 'I_n -> bool -> Type :=
+  | SplitLo (j : 'I_m) of i = j :> nat     : split_spec i (inl _ j) true
+  | SplitHi (k : 'I_n) of i = m + k :> nat : split_spec i (inr _ k) false.
+
+Lemma splitP m n (i : 'I_(m + n)) : split_spec i (split i) (i < m).
+Admitted.
+
+Variant split_ord_spec m n (i : 'I_(m + n)) : 'I_m + 'I_n -> bool -> Type :=
+  | SplitOrdLo (j : 'I_m) of i = lshift _ j : split_ord_spec i (inl _ j) true
+  | SplitOrdHi (k : 'I_n) of i = rshift _ k : split_ord_spec i (inr _ k) false.
+
+Lemma split_ordP m n (i : 'I_(m + n)) : split_ord_spec i (split i) (i < m).
+Admitted.
+
+Definition unsplit {m n} (jk : 'I_m + 'I_n) :=
+  match jk with inl j => lshift n j | inr k => rshift m k end.
+
+Lemma ltn_unsplit m n (jk : 'I_m + 'I_n) : (unsplit jk < m) = jk.
+Admitted.
+
+Lemma splitK {m n} : cancel (@split m n) unsplit.
+Admitted.
+
+Lemma unsplitK {m n} : cancel (@unsplit m n) split.
+Admitted.
+
+Section OrdinalPos.
+
+Variable n' : nat.
+Local Notation n := n'.+1.
+
+Definition ord0 := Ordinal (ltn0Sn n').
+Definition ord_max := Ordinal (ltnSn n').
+
+Lemma leq_ord (i : 'I_n) : i <= n'.
+Admitted.
+
+Lemma sub_ord_proof m : n' - m < n.
+Admitted.
+Definition sub_ord m := Ordinal (sub_ord_proof m).
+
+Lemma sub_ordK (i : 'I_n) : n' - (n' - i) = i.
+Admitted.
+
+Definition inord m : 'I_n := insubd ord0 m.
+
+Lemma inordK m : m < n -> inord m = m :> nat.
+Admitted.
+
+Lemma inord_val (i : 'I_n) : inord i = i.
+Admitted.
+
+Lemma enum_ordSl : enum 'I_n = ord0 :: map (lift ord0) (enum 'I_n').
+Admitted.
+
+Lemma enum_ordSr :
+  enum 'I_n = rcons (map (widen_ord (leqnSn _)) (enum 'I_n')) ord_max.
+Admitted.
+
+Lemma lift_max (i : 'I_n') : lift ord_max i = i :> nat.
+Admitted.
+
+Lemma lift0 (i : 'I_n') : lift ord0 i = i.+1 :> nat.
+Admitted.
+
+End OrdinalPos.
+
+Arguments ord0 {n'}.
+Arguments ord_max {n'}.
+Arguments inord {n'}.
+Arguments sub_ord {n'}.
+Arguments sub_ordK {n'}.
+Arguments inord_val {n'}.
+
+#[deprecated(since="mathcomp 1.15.0", note="Use enum_ordSl instead.")]
+Notation enum_ordS := enum_ordSl.
+
+Lemma ord1 : all_equal_to (ord0 : 'I_1).
+Admitted.
+
+ 
+Section ProdFinType.
+
+Variable T1 T2 : finType.
+
+Definition prod_enum := [seq (x1, x2) | x1 <- enum T1, x2 <- enum T2].
+
+Lemma predX_prod_enum (A1 : {pred T1}) (A2 : {pred T2}) :
+  count [predX A1 & A2] prod_enum = #|A1| * #|A2|.
+Admitted.
+
+Lemma prod_enumP : Finite.axiom prod_enum.
+Admitted.
+
+HB.instance Definition _ := isFinite.Build (T1 * T2)%type prod_enumP.
+
+Lemma cardX (A1 : {pred T1}) (A2 : {pred T2}) :
+  #|[predX A1 & A2]| = #|A1| * #|A2|.
+Admitted.
+
+Lemma card_prod : #|{: T1 * T2}| = #|T1| * #|T2|.
+Admitted.
+
+Lemma eq_card_prod (A : {pred (T1 * T2)}) : A =i predT -> #|A| = #|T1| * #|T2|.
+Admitted.
+
+End ProdFinType.
+
+Section TagFinType.
+
+Variables (I : finType) (T_ : I -> finType).
+
+Definition tag_enum :=
+  flatten [seq [seq Tagged T_ x | x <- enumF (T_ i)] | i <- enumF I].
+
+Lemma tag_enumP : Finite.axiom tag_enum.
+Admitted.
+
+HB.instance Definition _ := isFinite.Build {i : I & T_ i} tag_enumP.
+
+Lemma card_tagged :
+  #|{: {i : I & T_ i}}| = sumn (map (fun i => #|T_ i|) (enum I)).
+Admitted.
+
+End TagFinType.
+
+Section SumFinType.
+
+Variables T1 T2 : finType.
+
+Definition sum_enum :=
+  [seq inl _ x | x <- enumF T1] ++ [seq inr _ y | y <- enumF T2].
+
+Lemma sum_enum_uniq : uniq sum_enum.
+Admitted.
+
+Lemma mem_sum_enum u : u \in sum_enum.
+Admitted.
+
+HB.instance Definition sum_isFinite := isFinite.Build (T1 + T2)%type
+  (Finite.uniq_enumP sum_enum_uniq mem_sum_enum).
+
+Lemma card_sum : #|{: T1 + T2}| = #|T1| + #|T2|.
+Admitted.
+
+End SumFinType.
+
+End fintype.
+
+End mathcomp_DOT_ssreflect_DOT_fintype_WRAPPED.
+Module Export mathcomp_DOT_ssreflect_DOT_fintype.
+Module Export mathcomp.
+Module Export ssreflect.
+Module fintype.
+Include mathcomp_DOT_ssreflect_DOT_fintype_WRAPPED.fintype.
+End fintype.
+
+End ssreflect.
+
+End mathcomp.
+
+End mathcomp_DOT_ssreflect_DOT_fintype.
+Axiom proof_admitted : False.
+Tactic Notation "admit" := abstract case proof_admitted.
+
+Module mathcomp_DOT_ssreflect_DOT_tuple_WRAPPED.
+Module Export tuple.
+
+Import HB.structures.
+Import mathcomp.ssreflect.ssreflect.
+Import mathcomp.ssreflect.ssrbool.
+Import mathcomp.ssreflect.eqtype.
+Import mathcomp.ssreflect.ssrnat.
+Import mathcomp.ssreflect.seq.
+Import mathcomp.ssreflect.choice.
+Import mathcomp.ssreflect.fintype.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Section TupleDef.
+
+Variables (n : nat) (T : Type).
+
+Structure tuple_of : Type := Tuple {tval :> seq T; _ : size tval == n}.
+
+HB.instance Definition _ := [isSub for tval].
+
+Definition tuple t mkT : tuple_of :=
+  mkT (let: Tuple _ tP := t return size t == n in tP).
+
+End TupleDef.
+
+Notation "n .-tuple" := (tuple_of n)
+  (at level 2, format "n .-tuple") : type_scope.
+
+Notation "[ 'tuple' 'of' s ]" := (tuple (fun sP => @Tuple _ _ s sP))
+  (at level 0, format "[ 'tuple'  'of'  s ]") : form_scope.
+
+Section SeqTuple.
+
+Variables (n m : nat) (T U rT : Type).
+Implicit Type t : n.-tuple T.
+
+Lemma map_tupleP f t : @size rT (map f t) == n.
+admit.
+Defined.
+Canonical map_tuple f t := Tuple (map_tupleP f t).
+
+End SeqTuple.
+
+HB.instance Definition _ n (T : countType) :=
+  [Countable of n.-tuple T by <:].
+
+Module Type FinTupleSig.
+Section FinTupleSig.
+Variables (n : nat) (T : finType).
+Parameter enum : seq (n.-tuple T).
+Axiom enumP : Finite.axiom enum.
+End FinTupleSig.
+End FinTupleSig.
+
+Module FinTuple : FinTupleSig.
+Section FinTuple.
+Variables (n : nat) (T : finType).
+Definition enum : seq (n.-tuple T).
+Admitted.
+
+Lemma enumP : Finite.axiom enum.
+Admitted.
+
+End FinTuple.
+End FinTuple.
+
+Section UseFinTuple.
+
+Variables (n : nat) (T : finType).
+
+HB.instance Definition _ := isFinite.Build (n.-tuple T) (@FinTuple.enumP n T).
+
+Lemma enum_tupleP (A : {pred T}) : size (enum A) == #|A|.
+admit.
+Defined.
+Canonical enum_tuple A := Tuple (enum_tupleP A).
+
+Section ImageTuple.
+
+Variables (T' : Type) (f : T -> T') (A : {pred T}).
+Canonical codom_tuple : #|T|.-tuple T'.
+exact ([tuple of codom f]).
+Defined.
+
+End ImageTuple.
+
+End UseFinTuple.
+
+End tuple.
+
+End mathcomp_DOT_ssreflect_DOT_tuple_WRAPPED.
+Module Export mathcomp.
+Module Export ssreflect.
+Module tuple.
+Include mathcomp_DOT_ssreflect_DOT_tuple_WRAPPED.tuple.
+End tuple.
+Module Export finfun.
+
+Import HB.structures.
+Import mathcomp.ssreflect.ssreflect.
+Import mathcomp.ssreflect.ssrfun.
+Import mathcomp.ssreflect.ssrbool.
+Import mathcomp.ssreflect.eqtype.
+Import mathcomp.ssreflect.seq.
+Import mathcomp.ssreflect.choice.
+Import mathcomp.ssreflect.fintype.
+Import mathcomp.ssreflect.tuple.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Section Def.
+
+Variables (aT : finType) (rT : aT -> Type).
+
+Inductive finfun_on : seq aT -> Type :=
+| finfun_nil                            : finfun_on [::]
+| finfun_cons x s of rT x & finfun_on s : finfun_on (x :: s).
+Local Fixpoint finfun_rec (g : forall x, rT x) s : finfun_on s.
+Admitted.
+
+Local Fixpoint fun_of_fin_rec x s (f_s : finfun_on s) : x \in s -> rT x :=
+  if f_s is finfun_cons x1 s1 y1 f_s1 then
+    if eqP is ReflectT Dx in reflect _ Dxb return Dxb || (x \in s1) -> rT x then
+      fun=> ecast x (rT x) (esym Dx) y1
+    else fun_of_fin_rec f_s1
+  else fun isF =>  False_rect (rT x) (notF isF).
+
+Variant finfun_of (ph : phant (forall x, rT x)) : predArgType :=
+  FinfunOf of finfun_on (enum aT).
+
+Definition dfinfun_of ph := finfun_of ph.
+
+Definition fun_of_fin ph (f : finfun_of ph) x :=
+  let: FinfunOf f_aT := f in fun_of_fin_rec f_aT (mem_enum aT x).
+
+End Def.
+
+Coercion fun_of_fin : finfun_of >-> Funclass.
+
+Notation "{ 'ffun' fT }" := (finfun_of (Phant fT))
+  (at level 0, format "{ 'ffun'  '[hv' fT ']' }") : type_scope.
+
+Notation "{ 'dffun' fT }" := (dfinfun_of (Phant fT))
+  (at level 0, format "{ 'dffun'  '[hv' fT ']' }") : type_scope.
+
+Local Notation finPi aT rT := (forall x : Finite.sort aT, rT x) (only parsing).
+
+HB.lock Definition finfun aT rT g :=
+  FinfunOf (Phant (finPi aT rT)) (finfun_rec g (enum aT)).
+
+Section DepPlainTheory.
+Variables (aT : finType) (rT : aT -> Type).
+Notation fT := {ffun finPi aT rT}.
+Implicit Type f : fT.
+
+Definition total_fun g x := Tagged rT (g x : rT x).
+
+Definition tfgraph f := codom_tuple (total_fun f).
+Local Definition tfgraph_inv (G : #|aT|.-tuple {x : aT & rT x}) : option fT.
+Admitted.
+
+Local Lemma tfgraphK : pcancel tfgraph tfgraph_inv.
+Admitted.
+
+End DepPlainTheory.
+Arguments tfgraphK {aT rT} f : rename.
+
+Section InheritedStructures.
+
+Variable aT : finType.
+Notation dffun_aT rT rS := {dffun forall x : aT, rT x : rS}.
+
+#[hnf] HB.instance Definition _ rT := Finite.copy (dffun_aT rT finType)
+  (pcan_type tfgraphK).
+#[hnf] HB.instance Definition _ (rT : finType) :=
+  Finite.copy {ffun aT -> rT} {dffun forall _, rT}.
+
+End InheritedStructures.
+
+End finfun.
+
+Import HB.structures.
+Import mathcomp.ssreflect.ssreflect.
+Import mathcomp.ssreflect.ssrbool.
+Import mathcomp.ssreflect.ssrfun.
+Import mathcomp.ssreflect.seq.
+Import mathcomp.ssreflect.fintype.
+
+Set Implicit Arguments.
+
+Declare Scope big_scope.
+Reserved Notation "\big [ op / idx ]_ ( i | P ) F"
+  (at level 36, F at level 36, op, idx at level 10, i at level 50,
+           format "'[' \big [ op / idx ]_ ( i  |  P ) '/  '  F ']'").
+Reserved Notation "\big [ op / idx ]_ ( i : t | P ) F"
+  (at level 36, F at level 36, op, idx at level 10, i at level 50,
+           format "'[' \big [ op / idx ]_ ( i   :  t   |  P ) '/  '  F ']'").
+Reserved Notation "\big [ op / idx ]_ ( i 'in' A ) F"
+  (at level 36, F at level 36, op, idx at level 10, i, A at level 50,
+           format "'[' \big [ op / idx ]_ ( i  'in'  A ) '/  '  F ']'").
+Reserved Notation "\bigcup_ ( i : t | P ) F"
+  (at level 41, F at level 41, i at level 50,
+           format "'[' \bigcup_ ( i   :  t   |  P ) '/  '  F ']'").
+Reserved Notation "\bigcap_ ( i | P ) F"
+  (at level 41, F at level 41, i at level 50,
+           format "'[' \bigcap_ ( i  |  P ) '/  '  F ']'").
+Reserved Notation "\bigcap_ ( i : t | P ) F"
+  (at level 41, F at level 41, i at level 50,
+           format "'[' \bigcap_ ( i   :  t   |  P ) '/  '  F ']'").
+Reserved Notation "\bigcap_ ( i 'in' A ) F"
+  (at level 41, F at level 41, i, A at level 50,
+           format "'[' \bigcap_ ( i  'in'  A ) '/  '  F ']'").
+
+Module Export SemiGroup.
+
+HB.mixin Record isLaw T (op : T -> T -> T) := {
+  opA : associative op;
+}.
+
+HB.factory Record isComLaw T (op : T -> T -> T) := {
+  opA : associative op;
+  opC : commutative op;
+}.
+
+HB.builders Context T op of isComLaw T op.
+
+HB.instance Definition _ := isLaw.Build T op opA.
+
+HB.end.
+
+Module Import Exports.
+End Exports.
+
+End SemiGroup.
+
+HB.factory Record isLaw T (idm : T) (op : T -> T -> T) := {
+  opA : associative op;
+  op1m : left_id idm op;
+  opm1 : right_id idm op;
+}.
+
+HB.builders Context T idm op of isLaw T idm op.
+
+HB.instance Definition _ := SemiGroup.isLaw.Build T op opA.
+
+HB.end.
+
+HB.factory Record isComLaw T (idm : T) (op : T -> T -> T) := {
+  opA : associative op;
+  opC : commutative op;
+  op1m : left_id idm op;
+}.
+
+HB.builders Context T idm op of isComLaw T idm op.
+
+Lemma opm1 : right_id idm op.
+Admitted.
+
+HB.instance Definition _ := isLaw.Build T idm op opA op1m opm1.
+
+HB.end.
+
+Open Scope big_scope.
+
+Variant bigbody R I := BigBody of I & (R -> R -> R) & bool & R.
+
+Definition applybig {R I} (body : bigbody R I) x :=
+  let: BigBody _ op b v := body in if b then op v x else x.
+
+Definition reducebig R I idx r (body : I -> bigbody R I) :=
+  foldr (applybig \o body) idx r.
+
+HB.lock Definition bigop := reducebig.
+
+Fact index_enum_key : unit.
+Admitted.
+
+Definition index_enum (T : finType) :=
+  locked_with index_enum_key (Finite.enum T).
+Notation "\big [ op / idx ]_ ( i | P ) F" :=
+  (bigop idx (index_enum _) (fun i => BigBody i op P%B F)) : big_scope.
+Notation "\big [ op / idx ]_ ( i : t | P ) F" :=
+  (bigop idx (index_enum _) (fun i : t => BigBody i op P%B F))
+     (only parsing) : big_scope.
+Notation "\big [ op / idx ]_ ( i 'in' A ) F" :=
+  (\big[op/idx]_(i | i \in A) F) : big_scope.
+
+Import mathcomp.ssreflect.eqtype.
+Import mathcomp.ssreflect.choice.
+Unset Strict Implicit.
+
+Section SetType.
+
+Variable T : finType.
+
+Inductive set_type : predArgType := FinSet of {ffun pred T}.
+Definition finfun_of_set A := let: FinSet f := A in f.
+Definition set_of of phant T := set_type.
+Identity Coercion type_of_set_of : set_of >-> set_type.
+
+Definition set_isSub := Eval hnf in [isNew for finfun_of_set].
+HB.instance Definition _ := set_isSub.
+HB.instance Definition _ := [Finite of set_type by <:].
+
+End SetType.
+
+Delimit Scope set_scope with SET.
+Open Scope set_scope.
+
+Notation "{ 'set' T }" := (set_of (Phant T))
+  (at level 0, format "{ 'set'  T }") : type_scope.
+Notation "A :==: B" := (A == B :> {set _})
+  (at level 70, no associativity, only parsing) : set_scope.
+Notation "A :!=: B" := (A != B :> {set _})
+  (at level 70, no associativity, only parsing) : set_scope.
+
+HB.lock
+Definition finset (T : finType) (P : pred T) : {set T} := @FinSet T (finfun P).
+
+HB.lock
+Definition pred_of_set T (A : set_type T) : fin_pred_sort (predPredType T)
+:= val A.
+
+Notation "[ 'set' x : T | P ]" := (finset (fun x : T => P%B))
+  (at level 0, x at level 99, only parsing) : set_scope.
+Notation "[ 'set' x | P ]" := [set x : _ | P]
+  (at level 0, x, P at level 99, format "[ 'set'  x  |  P ]") : set_scope.
+Notation "[ 'set' x 'in' A ]" := [set x | x \in A]
+  (at level 0, x at level 99, format "[ 'set'  x  'in'  A ]") : set_scope.
+Notation "[ 'set' x | P & Q ]" := [set x | P && Q ]
+  (at level 0, x, P at level 99, format "[ 'set'  x  |  P  &  Q ]") : set_scope.
+Notation "[ 'set' x 'in' A | P ]" := [set x | x \in A & P]
+  (at level 0, x at level 99, format "[ 'set'  x  'in'  A  |  P ]") : set_scope.
+
+Coercion pred_of_set: set_type >-> fin_pred_sort.
+
+Section BasicSetTheory.
+
+Variable T : finType.
+
+Definition set0 := [set x : T | false].
+Definition setTfor (phT : phant T) := [set x : T | true].
+
+End BasicSetTheory.
+
+Arguments set0 {T}.
+
+Notation "[ 'set' : T ]" := (setTfor (Phant T))
+  (at level 0, format "[ 'set' :  T ]") : set_scope.
+
+Notation setT := [set: _] (only parsing).
+
+HB.lock
+Definition set1 (T : finType) (a : T) := [set x | x == a].
+
+Section setOpsDefs.
+
+Variable T : finType.
+Implicit Types (a x : T) (A B D : {set T}) (P : {set {set T}}).
+
+Definition setU A B := [set x | (x \in A) || (x \in B)].
+Definition setI A B := [set x in A | x \in B].
+Definition setC A := [set x | x \notin A].
+Definition setD A B := [set x | x \notin B & x \in A].
+
+End setOpsDefs.
+
+Notation "[ 'set' a ]" := (set1 a)
+  (at level 0, a at level 99, format "[ 'set'  a ]") : set_scope.
+Notation "A :&: B" := (setI A B) : set_scope.
+Notation "~: A" := (setC A) (at level 35, right associativity) : set_scope.
+Notation "A :\: B" := (setD A B) : set_scope.
+
+HB.lock
+Definition imset (aT rT : finType) f mD := [set y in @image_mem aT rT f mD].
+
+HB.lock
+Definition imset2 (aT1 aT2 rT : finType) f (D1 : mem_pred aT1) (D2 : _ -> mem_pred aT2) :=
+  [set y in @image_mem _ rT (uncurry f) (mem [pred u | D1 u.1 & D2 u.1 u.2])].
+
+Definition preimset (aT : finType) rT f (R : mem_pred rT) :=
+  [set x : aT | in_mem (f x) R].
+
+Notation "f @^-1: A" := (preimset f (mem A)) (at level 24) : set_scope.
+Notation "f @: A" := (imset f (mem A)) (at level 24) : set_scope.
+Notation "f @2: ( A , B )" := (imset2 f (mem A) (fun _ => mem B))
+  (at level 24, format "f  @2:  ( A ,  B )") : set_scope.
+
+Notation "\bigcup_ ( i : t | P ) F" :=
+  (\big[@setU _/set0]_(i : t | P%B) F%SET) (only parsing): set_scope.
+Notation "\bigcap_ ( i | P ) F" :=
+  (\big[@setI _/setT]_(i | P%B) F%SET) : set_scope.
+Notation "\bigcap_ ( i : t | P ) F" :=
+  (\big[@setI _/setT]_(i : t | P%B) F%SET) (only parsing): set_scope.
+Notation "\bigcap_ ( i 'in' A ) F" :=
+  (\big[@setI _/setT]_(i in A) F%SET) : set_scope.
+
+Section MaxSetMinSet.
+
+Variable T : finType.
+Notation sT := {set T}.
+Implicit Types A B C : sT.
+
+Definition minset P A := [forall (B : sT | B \subset A), (B == A) == P B].
+
+Fact maxset_key : unit.
+Admitted.
+Definition maxset P A :=
+  minset (fun B => locked_with maxset_key P (~: B)) (~: A).
+
+End MaxSetMinSet.
+
+Import mathcomp.ssreflect.ssrnat.
+Import mathcomp.ssreflect.div.
+
+Fixpoint edivn2 q r := if r is r'.+2 then edivn2 q.+1 r' else (q, r).
+
+Fixpoint elogn2 e q r {struct q} :=
+  match q, r with
+  | 0, _ | _, 0 => (e, q)
+  | q'.+1, 1 => elogn2 e.+1 q' q'
+  | q'.+1, r'.+2 => elogn2 e q' r'
+  end.
+
+Definition ifnz T n (x y : T) := if n is 0 then y else x.
+
+Definition cons_pfactor (p e : nat) pd := ifnz e ((p, e) :: pd) pd.
+
+Notation "p ^? e :: pd" := (cons_pfactor p e pd)
+  (at level 30, e at level 30, pd at level 60) : nat_scope.
+
+Section prime_decomp.
+
+Local Fixpoint prime_decomp_rec m k a b c e :=
+  let p := k.*2.+1 in
+  if a is a'.+1 then
+    if b - (ifnz e 1 k - c) is b'.+1 then
+      [rec m, k, a', b', ifnz c c.-1 (ifnz e p.-2 1), e] else
+    if (b == 0) && (c == 0) then
+      let b' := k + a' in [rec b'.*2.+3, k, a', b', k.-1, e.+1] else
+    let bc' := ifnz e (ifnz b (k, 0) (edivn2 0 c)) (b, c) in
+    p ^? e :: ifnz a' [rec m, k.+1, a'.-1, bc'.1 + a', bc'.2, 0] [:: (m, 1)]
+  else if (b == 0) && (c == 0) then [:: (p, e.+2)] else p ^? e :: [:: (m, 1)]
+where "[ 'rec' m , k , a , b , c , e ]" := (prime_decomp_rec m k a b c e).
+
+Definition prime_decomp n :=
+  let: (e2, m2) := elogn2 0 n.-1 n.-1 in
+  if m2 < 2 then 2 ^? e2 :: 3 ^? m2 :: [::] else
+  let: (a, bc) := edivn m2.-2 3 in
+  let: (b, c) := edivn (2 - bc) 2 in
+  2 ^? e2 :: [rec m2.*2.+1, 1, a, b, c, 0].
+
+End prime_decomp.
+
+Definition primes n := unzip1 (prime_decomp n).
+
+Definition nat_pred := simpl_pred nat.
+
+Definition pdiv n := head 1 (primes n).
+Coercion nat_pred_of_nat (p : nat) : nat_pred.
+Admitted.
+
+Section NatPreds.
+
+Variables (n : nat) (pi : nat_pred).
+Definition negn : nat_pred.
+exact ([predC pi]).
+Defined.
+Definition pnat : pred nat.
+exact (fun m => (m > 0) && all [in pi] (primes m)).
+Defined.
+
+End NatPreds.
+
+Notation "pi ^'" := (negn pi) (at level 2, format "pi ^'") : nat_scope.
+
+Notation "pi .-nat" := (pnat pi) (at level 2, format "pi .-nat") : nat_scope.
+
+Declare Scope group_scope.
+Delimit Scope Group_scope with G.
+Open Scope group_scope.
+Reserved Notation "#| B : A |" (at level 0, B, A at level 99,
+  format "#| B  :  A |").
+Reserved Notation "A <| B" (at level 70, no associativity).
+
+HB.mixin Record isMulBaseGroup G := {
+  mulg_subdef : G -> G -> G;
+  oneg_subdef : G;
+  invg_subdef : G -> G;
+  mulgA_subproof : associative mulg_subdef ;
+  mul1g_subproof : left_id oneg_subdef  mulg_subdef ;
+  invgK_subproof : involutive invg_subdef ;
+  invMg_subproof : {morph invg_subdef  : x y / mulg_subdef  x y >-> mulg_subdef  y x}
+}.
+
+#[arg_sort, short(type="baseFinGroupType")]
+HB.structure Definition BaseFinGroup := { G of isMulBaseGroup G & Finite G }.
+Section ElementOps.
+
+Variable T : baseFinGroupType.
+Notation rT := (BaseFinGroup.sort T).
+
+Definition oneg : rT := Eval unfold oneg_subdef in @oneg_subdef T.
+Definition mulg : T -> T -> rT := Eval unfold mulg_subdef in @mulg_subdef T.
+Definition invg : T -> rT := Eval unfold invg_subdef in @invg_subdef T.
+Definition expgn_rec (x : T) n : rT := iterop n mulg x oneg.
+
+End ElementOps.
+
+Definition expgn := nosimpl expgn_rec.
+
+Notation "1" := (@oneg _) : group_scope.
+Notation "x1 * x2" := (mulg x1 x2) : group_scope.
+Notation "x ^-1" := (invg x) : group_scope.
+
+HB.mixin Record BaseFinGroup_isGroup G of BaseFinGroup G := {
+  mulVg_subproof : left_inverse (@oneg G) (@invg _) (@mulg _)
+}.
+
+#[short(type="finGroupType")]
+HB.structure Definition FinGroup :=
+  { G of BaseFinGroup_isGroup G & BaseFinGroup G }.
+
+HB.factory Record isMulGroup G of Finite G := {
+  mulg : G -> G -> G;
+  oneg : G;
+  invg : G -> G;
+  mulgA : associative mulg;
+  mul1g : left_id oneg mulg;
+  mulVg : left_inverse oneg invg mulg;
+}.
+
+HB.builders Context G of isMulGroup G.
+Infix "*" := mulg.
+
+Lemma mk_invgK : involutive invg.
+Admitted.
+
+Lemma mk_invMg : {morph invg : x y / x * y >-> y * x}.
+Admitted.
+
+HB.instance Definition _ :=
+  isMulBaseGroup.Build G mulgA mul1g mk_invgK mk_invMg.
+HB.instance Definition _ := BaseFinGroup_isGroup.Build G mulVg.
+
+HB.end.
+
+Definition conjg (T : finGroupType) (x y : T) := y^-1 * (x * y).
+Notation "x1 ^ x2" := (conjg x1 x2) : group_scope.
+
+Definition commg (T : finGroupType) (x y : T) := x^-1 * x ^ y.
+
+Prenex Implicits mulg invg expgn conjg commg.
+
+Section BaseSetMulDef.
+
+Variable gT : baseFinGroupType.
+Implicit Types A B : {set gT}.
+
+Definition set_mulg A B := mulg @2: (A, B).
+Definition set_invg A := invg @^-1: A.
+
+Lemma set_mul1g : left_id [set 1] set_mulg.
+Admitted.
+
+Lemma set_mulgA : associative set_mulg.
+Admitted.
+
+Lemma set_invgK : involutive set_invg.
+Admitted.
+
+Lemma set_invgM : {morph set_invg : A B / set_mulg A B >-> set_mulg B A}.
+Admitted.
+
+HB.instance Definition set_base_group := isMulBaseGroup.Build (set_type gT)
+  set_mulgA set_mul1g set_invgK set_invgM.
+
+End BaseSetMulDef.
+
+Module Export GroupSet.
+Definition sort (gT : baseFinGroupType) := {set gT}.
+End GroupSet.
+Identity Coercion GroupSet_of_sort : GroupSet.sort >-> set_of.
+
+Module Type GroupSetBaseGroupSig.
+Definition sort (gT : baseFinGroupType) := BaseFinGroup.arg_sort {set gT}.
+End GroupSetBaseGroupSig.
+
+Module MakeGroupSetBaseGroup (Gset_base : GroupSetBaseGroupSig).
+Identity Coercion of_sort : Gset_base.sort >-> BaseFinGroup.arg_sort.
+End MakeGroupSetBaseGroup.
+
+Module Export GroupSetBaseGroup := MakeGroupSetBaseGroup GroupSet.
+
+Section GroupSetMulDef.
+
+Variable gT : finGroupType.
+Implicit Types A B : {set gT}.
+Definition rcoset A x := mulg^~ x @: A.
+Definition rcosets A B := rcoset A @: B.
+Definition indexg B A := #|rcosets A B|.
+
+Definition conjugate A x := conjg^~ x @: A.
+
+Definition commg_set A B := commg @2: (A, B).
+
+Definition normaliser A := [set x | conjugate A x \subset A].
+Definition centraliser A := \bigcap_(x in A) normaliser [set x].
+Definition abelian A := A \subset centraliser A.
+Definition normal A B := (A \subset B) && (B \subset normaliser A).
+
+End GroupSetMulDef.
+
+Notation "#| B : A |" := (indexg B A) : group_scope.
+
+Notation "''N' ( A )" := (normaliser A) : group_scope.
+Notation "A <| B" := (normal A B) : group_scope.
+
+Section GroupSetMulProp.
+
+Variable gT : finGroupType.
+Implicit Types A B C D : {set gT}.
+
+Definition group_set A := (1 \in A) && (A * A \subset A).
+
+Structure group_type : Type := Group {
+  gval :> GroupSet.sort gT;
+  _ : group_set gval
+}.
+Definition group_of of phant gT : predArgType.
+exact (group_type).
+Defined.
+Local Notation groupT := (group_of (Phant gT)).
+
+HB.instance Definition _ := [isSub for gval].
+#[hnf] HB.instance Definition _ := [Finite of group_type by <:].
+
+Definition group (A : {set gT}) gA : groupT := @Group A gA.
+
+End GroupSetMulProp.
+
+Notation "{ 'group' gT }" := (group_of (Phant gT))
+  (at level 0, format "{ 'group'  gT }") : type_scope.
+
+HB.lock
+Definition generated (gT : finGroupType) (A : {set gT}) :=
+  \bigcap_(G : {group gT} | A \subset G) G.
+Definition commutator (gT : finGroupType) (A B : {set gT}) := generated (commg_set A B).
+Notation "<< A >>"  := (generated A) : group_scope.
+Notation "[ ~: A1 , A2 , .. , An ]" :=
+  (commutator .. (commutator A1 A2) .. An) : group_scope.
+
+Section GroupInter.
+
+Variable gT : finGroupType.
+
+Lemma group_set_generated (A : {set gT}) : group_set <<A>>.
+Admitted.
+
+Canonical generated_group A := group (group_set_generated A).
+
+End GroupInter.
+
+Section MinMaxGroup.
+
+Variable gT : finGroupType.
+Implicit Types gP : pred {group gT}.
+
+Definition maxgroup A gP := maxset (fun A => group_set A && gP <<A>>%G) A.
+Definition mingroup A gP := minset (fun A => group_set A && gP <<A>>%G) A.
+
+End MinMaxGroup.
+
+Notation "[ 'max' A 'of' G | gP ]" :=
+  (maxgroup A (fun G : {group _} => gP)) : group_scope.
+Notation "[ 'max' G | gP ]" := [max gval G of G | gP] : group_scope.
+Notation "[ 'min' A 'of' G | gP ]" :=
+  (mingroup A (fun G : {group _} => gP)) : group_scope.
+Notation "[ 'min' A 'of' G | gP & gQ ]" :=
+  [min A of G | gP && gQ] : group_scope.
+
+Section Cosets.
+
+Variables (gT : finGroupType) (Q A : {set gT}).
+
+Notation H := <<A>>.
+Definition coset_range := [pred B in rcosets H 'N(A)].
+
+Record coset_of : Type :=
+  Coset { set_of_coset :> GroupSet.sort gT; _ : coset_range set_of_coset }.
+
+HB.instance Definition _ := [isSub for set_of_coset].
+#[hnf] HB.instance Definition _ := [Finite of coset_of by <:].
+
+Lemma coset_one_proof : coset_range H.
+admit.
+Defined.
+Definition coset_one := Coset coset_one_proof.
+
+Lemma coset_range_mul (B C : coset_of) : coset_range (B * C).
+admit.
+Defined.
+
+Definition coset_mul B C := Coset (coset_range_mul B C).
+
+Lemma coset_range_inv (B : coset_of) : coset_range B^-1.
+admit.
+Defined.
+
+Definition coset_inv B := Coset (coset_range_inv B).
+
+Lemma coset_mulP : associative coset_mul.
+admit.
+Defined.
+
+Lemma coset_oneP : left_id coset_one coset_mul.
+admit.
+Defined.
+
+Lemma coset_invP : left_inverse coset_one coset_inv coset_mul.
+admit.
+Defined.
+
+HB.instance Definition _ :=
+  isMulGroup.Build coset_of coset_mulP coset_oneP coset_invP.
+Definition quotient : {set coset_of}.
+Admitted.
+
+End Cosets.
+
+Notation "A / H" := (quotient A H) : group_scope.
+
+Section PgroupDefs.
+
+Variable gT : finGroupType.
+Implicit Type (x : gT) (A B : {set gT}) (pi : nat_pred) (p n : nat).
+
+Definition pgroup pi A := pi.-nat #|A|.
+
+Definition psubgroup pi A B := (B \subset A) && pgroup pi B.
+
+Definition p_group A := pgroup (pdiv #|A|) A.
+
+Definition Hall A B := (B \subset A) && coprime #|B| #|A : B|.
+
+Definition pHall pi A B := [&& B \subset A, pgroup pi B & pi^'.-nat #|A : B|].
+
+Definition Sylow A B := p_group B && Hall A B.
+
+End PgroupDefs.
+
+Notation "pi .-group" := (pgroup pi)
+  (at level 2, format "pi .-group") : group_scope.
+
+Notation "pi .-subgroup ( A )" := (psubgroup pi A)
+  (at level 8, format "pi .-subgroup ( A )") : group_scope.
+
+Notation "pi .-Hall ( G )" := (pHall pi G)
+  (at level 8, format "pi .-Hall ( G )") : group_scope.
+
+Notation "p .-Sylow ( G )" := (nat_pred_of_nat p).-Hall(G)
+  (at level 8, format "p .-Sylow ( G )") : group_scope.
+
+Section PcoreDef.
+
+Variables (pi : nat_pred) (gT : finGroupType) (A : {set gT}).
+
+Definition pcore := \bigcap_(G | [max G | pi.-subgroup(A) G]) G.
+
+End PcoreDef.
+Notation "''O_' pi ( G )" := (pcore pi G)
+  (at level 8, pi at level 2, format "''O_' pi ( G )") : group_scope.
+
+Definition derived_at_rec n (gT : finGroupType) (A : {set gT}) :=
+  iter n (fun B => [~: B, B]) A.
+
+Definition derived_at := nosimpl derived_at_rec.
+Notation "G ^` ( n )" := (derived_at n G) : group_scope.
+
+Section GroupDefs.
+
+Variable gT : finGroupType.
+Implicit Types A B U V : {set gT}.
+
+Definition maximal A B := [max A of G | G \proper B].
+
+Definition minnormal A B := [min A of G | G :!=: 1 & B \subset 'N(G)].
+
+Definition simple A := minnormal A A.
+End GroupDefs.
+
+Section PropertiesDefs.
+
+Variables (gT : finGroupType) (A : {set gT}).
+
+Definition solvable :=
+  [forall (G : {group gT} | G \subset A :&: [~: G, G]), G :==: 1].
+
+End PropertiesDefs.
+
+HB.mixin Record IsMinSimpleOddGroup gT of FinGroup gT := {
+  mFT_odd_full : odd #|[set: gT]|;
+  mFT_simple : simple [set: gT];
+  mFT_nonSolvable : ~~ solvable [set: gT];
+  mFT_min : forall M : {group gT}, M \proper [set: gT] -> solvable M
+}.
+
+#[short(type="minSimpleOddGroupType")]
+HB.structure
+Definition minSimpleOddGroup := { G of IsMinSimpleOddGroup G & FinGroup G }.
+
+Notation TheMinSimpleOddGroup gT :=
+  [set: BaseFinGroup.arg_sort gT]
+  (only parsing).
+
+Section MinSimpleOdd.
+
+Variable gT : minSimpleOddGroupType.
+Notation G := (TheMinSimpleOddGroup gT).
+
+Definition minSimple_max_groups := [set M : {group gT} | maximal M G].
+
+End MinSimpleOdd.
+
+Notation "''M'" := (minSimple_max_groups _) : group_scope.
+Reserved Notation "M `_ \sigma" (at level 3, format "M `_ \sigma").
+
+Section Def.
+
+Variable gT : finGroupType.
+
+Variable M : {set gT}.
+
+Definition sigma :=
+  [pred p | [exists (P : {group gT} | p.-Sylow(M) P), 'N(P) \subset M]].
+Definition sigma_core := 'O_sigma(M).
+
+End Def.
+
+Notation "\sigma ( M )" := (sigma M) : group_scope.
+Notation "M `_ \sigma" := (sigma_core M) : group_scope.
+
+Section Definitons.
+
+Variable gT : minSimpleOddGroupType.
+Implicit Type M X : {set gT}.
+
+Fact kappa_key : unit.
+Admitted.
+Definition kappa_def M : nat_pred.
+Admitted.
+Definition kappa := locked_with kappa_key kappa_def.
+
+Definition sigma_kappa M := [predU \sigma(M) & kappa M].
+
+Definition TypeF_maxgroups := [set M in 'M | (kappa M)^'.-group M].
+
+Definition TypeP_maxgroups := 'M :\: TypeF_maxgroups.
+
+Definition TypeP1_maxgroups :=
+  [set M in TypeP_maxgroups | (sigma_kappa M).-group M].
+
+End Definitons.
+
+Notation "\kappa ( M )" := (kappa M)
+  (at level 8, format "\kappa ( M )") : group_scope.
+
+Notation "''M_' ''P1'" := (TypeP1_maxgroups _)
+  (at level 2, format "''M_' ''P1'") : group_scope.
+
+Section Definitions.
+
+Variables (gT : finGroupType) (M : {set gT}).
+
+Definition Fitting_core :=
+  <<\bigcup_(P : {group gT} | Sylow M P && (P <| M)) P>>.
+
+End Definitions.
+
+Notation "M `_ \F" := (Fitting_core M)
+  (at level 3, format "M `_ \F") : group_scope.
+
+Section Definitions.
+
+Variable gT : minSimpleOddGroupType.
+
+Implicit Types M U V W X : {set gT}.
+
+Definition FTtype M :=
+  if \kappa(M)^'.-group M then 1%N else
+  if M`_\sigma != M^`(1) then 2 else
+  if M`_\F == M`_\sigma then 5 else
+  if abelian (M`_\sigma / M`_\F) then 3 else 4.
+
+Definition FTcore M := if 0 < FTtype M <= 2 then M`_\F else M^`(1).
+
+End Definitions.
+
+Notation "M `_ \s" := (FTcore M) (at level 3, format "M `_ \s") : group_scope.
+
+Variable gT : minSimpleOddGroupType.
+
+Variable M : {group gT}.
+
+Lemma FTtype_P1max : (M \in 'M_'P1) = (2 < FTtype M <= 5).
+Admitted.
+
+Lemma Msigma_eq_der1 : M \in 'M_'P1 -> M`_\sigma = M^`(1).
+Admitted.
+
+Lemma Fcore_eq_FTcore : reflect (M`_\F = M`_\s) (FTtype M \in pred3 1%N 2 5).
+Proof.
+rewrite /FTcore -mem_iota 3!inE orbA; case type12M: (_ || _); first by left.
+move: type12M FTtype_P1max; rewrite /FTtype; do 2![case: ifP => // _] => _.
+rewrite !(fun_if (leq^~ 5)) !(fun_if (leq 3)) !if_same /= => P1maxM.
+rewrite Msigma_eq_der1 // !(fun_if (eq_op^~ 5)) if_same.
+by rewrite [if _ then _ else _]andbT; apply: eqP.
diff --git a/coqbot-request-stamp b/coqbot-request-stamp
index f747925..e1a93b8 100644
--- a/coqbot-request-stamp
+++ b/coqbot-request-stamp
@@ -1 +1 @@
-DUMMY
+PR_kwDOABUDh85VFaaq <> coq-community/run-coq-bug-minimizer run-coq-bug-minimizer-257712388571 coq coq 17836
\ No newline at end of file
diff --git a/coqbot.ci-target b/coqbot.ci-target
index 2359f92..aeb810e 100644
--- a/coqbot.ci-target
+++ b/coqbot.ci-target
@@ -1 +1 @@
-TAKE FROM failing-log.log
+ci-oddorder
diff --git a/coqbot.compiler b/coqbot.compiler
index 2da4316..1ac9092 100644
--- a/coqbot.compiler
+++ b/coqbot.compiler
@@ -1 +1 @@
-4.10.0
+4.14.1+flambda
diff --git a/coqbot.failing-artifact-urls b/coqbot.failing-artifact-urls
index 8b13789..d665531 100644
--- a/coqbot.failing-artifact-urls
+++ b/coqbot.failing-artifact-urls
@@ -1 +1 @@
-
+https://gitlab.inria.fr/coq/coq/-/jobs/3443131/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3443171/artifacts/download
diff --git a/coqbot.failing-sha b/coqbot.failing-sha
index 8b13789..a13ed0b 100644
--- a/coqbot.failing-sha
+++ b/coqbot.failing-sha
@@ -1 +1 @@
-
+1180a512534f19bca0e1e8fffc96f553cd279bf5
diff --git a/coqbot.issue-number b/coqbot.issue-number
index e69de29..fff31c8 100644
--- a/coqbot.issue-number
+++ b/coqbot.issue-number
@@ -0,0 +1 @@
+17836
diff --git a/coqbot.passing-artifact-urls b/coqbot.passing-artifact-urls
index 8b13789..d0c2522 100644
--- a/coqbot.passing-artifact-urls
+++ b/coqbot.passing-artifact-urls
@@ -1 +1 @@
-
+https://gitlab.inria.fr/coq/coq/-/jobs/3442633/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3442673/artifacts/download
diff --git a/coqbot.passing-sha b/coqbot.passing-sha
index 8b13789..0ccd9fb 100644
--- a/coqbot.passing-sha
+++ b/coqbot.passing-sha
@@ -1 +1 @@
-
+f1de96dc193b5889ba2ecbc9f276c3776e84248a
diff --git a/coqbot.resume-minimization-url b/coqbot.resume-minimization-url
new file mode 100644
index 0000000..4f09f09
--- /dev/null
+++ b/coqbot.resume-minimization-url
@@ -0,0 +1 @@
+https://coqbot.herokuapp.com/resume-ci-minimization
diff --git a/coqbot.resumption-args b/coqbot.resumption-args
new file mode 100644
index 0000000..abb8f40
--- /dev/null
+++ b/coqbot.resumption-args
@@ -0,0 +1,8 @@
+registry.gitlab.inria.fr/coq/coq:edge_ubuntu-V2023-08-28-93124ee272
+ci-oddorder
+4.14.1+flambda
+https://gitlab.inria.fr/coq/coq/-/jobs/3443131/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3443171/artifacts/download
+https://gitlab.inria.fr/coq/coq/-/jobs/3442633/artifacts/download https://gitlab.inria.fr/coq/coq/-/jobs/3442673/artifacts/download
+f1de96dc193b5889ba2ecbc9f276c3776e84248a
+1180a512534f19bca0e1e8fffc96f553cd279bf5
+
diff --git a/coqbot.url b/coqbot.url
index e69de29..fa1cbeb 100644
--- a/coqbot.url
+++ b/coqbot.url
@@ -0,0 +1 @@
+https://coqbot.herokuapp.com/ci-minimization