diff --git a/theories/All/All.v b/theories/All/All.v
index f816d62bac..191ae070b2 100644
--- a/theories/All/All.v
+++ b/theories/All/All.v
@@ -176,10 +176,7 @@ From Stdlib Require Export Strings.String.
 From Stdlib Require Export Streams.StreamMemo.
 From Stdlib Require Export Streams.Streams.
 From Stdlib Require Export Sorting.CPermutation.
-From Stdlib Require Export Sorting.Heap.
 From Stdlib Require Export Sorting.Mergesort.
-From Stdlib Require Export Sorting.PermutEq.
-From Stdlib Require Export Sorting.PermutSetoid.
 From Stdlib Require Export Sorting.Permutation.
 From Stdlib Require Export Sorting.SetoidList.
 From Stdlib Require Export Sorting.SetoidPermutation.
diff --git a/theories/Make.sorting b/theories/Make.sorting
index dd1d383381..55130f0b91 100644
--- a/theories/Make.sorting
+++ b/theories/Make.sorting
@@ -1,8 +1,5 @@
-Sorting/Heap.v
 Sorting/CPermutation.v
 Sorting/Mergesort.v
-Sorting/PermutSetoid.v
-Sorting/PermutEq.v
 Sorting/Sorting.v
 Sorting/Permutation.v
 Sorting/Sorted.v
diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
deleted file mode 100644
index 1c42f25fe0..0000000000
--- a/theories/Sorting/Heap.v
+++ /dev/null
@@ -1,322 +0,0 @@
-(************************************************************************)
-(*         *      The Rocq Prover / The Rocq Development Team           *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** This file is deprecated, for a tree on list, use [Mergesort.v]. *)
-
-(** A development of Treesort on Heap trees. It has an average
-    complexity of O(n.log n) but of O(n²) in the worst case (e.g. if
-    the list is already sorted) *)
-
-(* G. Huet 1-9-95 uses Multiset *)
-
-From Stdlib Require Import List Multiset PermutSetoid Relations Sorting.
-
-#[local]
-Set Warnings "-deprecated".
-
-Section defs.
-
-  (** * Trees and heap trees *)
-
-  (** ** Definition of trees over an ordered set *)
-
-  Variable A : Type.
-  Variable leA : relation A.
-  Variable eqA : relation A.
-
-  Let gtA (x y:A) := ~ leA x y.
-
-  Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}.
-  Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
-  Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
-  Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
-  Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.
-
-  #[local]
-  Hint Resolve leA_refl : core.
-  #[local]
-  Hint Immediate eqA_dec leA_dec leA_antisym : core.
-
-  Let emptyBag := EmptyBag A.
-  Let singletonBag := SingletonBag _ eqA_dec.
-
-  Inductive Tree :=
-    | Tree_Leaf : Tree
-    | Tree_Node : A -> Tree -> Tree -> Tree.
-
-  (** [a] is lower than a Tree [T] if [T] is a Leaf
-      or [T] is a Node holding [b>a] *)
-
-  #[deprecated(since="8.3", note="Use mergesort.v")]
-  Definition leA_Tree (a:A) (t:Tree) :=
-    match t with
-      | Tree_Leaf => True
-      | Tree_Node b T1 T2 => leA a b
-    end.
-
-  #[deprecated(since="8.3", note="Use mergesort.v")]
-  Lemma leA_Tree_Leaf : forall a:A, leA_Tree a Tree_Leaf.
-  Proof.
-    simpl; auto with datatypes.
-  Qed.
-
-  #[deprecated(since="8.3", note="Use mergesort.v")]
-  Lemma leA_Tree_Node :
-    forall (a b:A) (G D:Tree), leA a b -> leA_Tree a (Tree_Node b G D).
-  Proof.
-    simpl; auto with datatypes.
-  Qed.
-
-
-  (** ** The heap property *)
-
-  Inductive is_heap : Tree -> Prop :=
-    | nil_is_heap : is_heap Tree_Leaf
-    | node_is_heap :
-      forall (a:A) (T1 T2:Tree),
-        leA_Tree a T1 ->
-        leA_Tree a T2 ->
-        is_heap T1 -> is_heap T2 -> is_heap (Tree_Node a T1 T2).
-
-  #[deprecated(since="8.3", note="Use mergesort.v")]
-  Lemma invert_heap :
-    forall (a:A) (T1 T2:Tree),
-      is_heap (Tree_Node a T1 T2) ->
-      leA_Tree a T1 /\ leA_Tree a T2 /\ is_heap T1 /\ is_heap T2.
-  Proof.
-    intros; inversion H; auto with datatypes.
-  Qed.
-
-  (* This lemma ought to be generated automatically by the Inversion tools *)
-  #[deprecated(since="8.3", note="Use mergesort.v")]
-  Lemma is_heap_rect :
-    forall P:Tree -> Type,
-      P Tree_Leaf ->
-      (forall (a:A) (T1 T2:Tree),
-        leA_Tree a T1 ->
-        leA_Tree a T2 ->
-        is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
-      forall T:Tree, is_heap T -> P T.
-  Proof.
-    simple induction T; auto with datatypes.
-    intros a G PG D PD PN.
-    elim (invert_heap a G D); auto with datatypes.
-    intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
-    apply X0; auto with datatypes.
-  Qed.
-
-  (* This lemma ought to be generated automatically by the Inversion tools *)
-  #[deprecated(since="8.3", note="Use mergesort.v")]
-  Lemma is_heap_rec :
-    forall P:Tree -> Set,
-      P Tree_Leaf ->
-      (forall (a:A) (T1 T2:Tree),
-        leA_Tree a T1 ->
-        leA_Tree a T2 ->
-        is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
-      forall T:Tree, is_heap T -> P T.
-  Proof.
-    simple induction T; auto with datatypes.
-    intros a G PG D PD PN.
-    elim (invert_heap a G D); auto with datatypes.
-    intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
-    apply X; auto with datatypes.
-  Qed.
-
-  #[deprecated(since="8.3", note="Use mergesort.v")]
-  Lemma low_trans :
-    forall (T:Tree) (a b:A), leA a b -> leA_Tree b T -> leA_Tree a T.
-  Proof.
-    simple induction T; auto with datatypes.
-    intros; simpl; apply leA_trans with b; auto with datatypes.
-  Qed.
-
-  (** ** Merging two sorted lists *)
-
-   Inductive merge_lem (l1 l2:list A) : Type :=
-    merge_exist :
-    forall l:list A,
-      Sorted leA l ->
-      meq (list_contents _ eqA_dec l)
-      (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) ->
-      (forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) ->
-      merge_lem l1 l2.
-  Import Morphisms.
-
-  Instance: Equivalence (@meq A).
-  Proof. constructor; auto with datatypes. red. apply meq_trans. Defined.
-
-  Instance: Proper (@meq A ++> @meq _ ++> @meq _) (@munion A).
-  Proof. intros x y H x' y' H'. now apply meq_congr. Qed.
-
-  #[deprecated(since="8.3", note="Use mergesort.v")]
-  Lemma merge :
-    forall l1:list A, Sorted leA l1 ->
-    forall l2:list A, Sorted leA l2 -> merge_lem l1 l2.
-  Proof.
-    fix merge 1; intros; destruct l1.
-    - apply merge_exist with l2; auto with datatypes.
-    - rename l1 into l.
-      revert l2 H0. fix merge0 1. intros.
-      destruct l2 as [|a0 l0].
-      + apply merge_exist with (a :: l); simpl; auto with datatypes.
-      + induction (leA_dec a a0) as [Hle|Hle].
-
-        * (* 1 (leA a a0) *)
-          apply Sorted_inv in H. destruct H.
-          destruct (merge l H (a0 :: l0) H0) as [l1 H2 H3 H4].
-          apply merge_exist with (a :: l1).
-          -- clear merge merge0.
-             auto using cons_sort, cons_leA with datatypes.
-          -- simpl. rewrite H3. now rewrite munion_ass.
-          -- intros. apply cons_leA.
-             apply (@HdRel_inv _ leA) with l; trivial with datatypes.
-
-        * (* 2 (leA a0 a) *)
-          apply Sorted_inv in H0. destruct H0.
-          destruct (merge0 l0 H0) as [l1 H2 H3 H4]. clear merge merge0.
-          apply merge_exist with (a0 :: l1);
-            auto using cons_sort, cons_leA with datatypes.
-          -- simpl; rewrite H3. simpl. setoid_rewrite munion_ass at 1. rewrite munion_comm.
-             repeat rewrite munion_ass. setoid_rewrite munion_comm at 3. reflexivity.
-          -- intros. apply cons_leA.
-             apply (@HdRel_inv _ leA) with l0; trivial with datatypes.
-  Qed.
-
-  (** ** From trees to multisets *)
-
-  (** contents of a tree as a multiset *)
-
-  (** Nota Bene : In what follows the definition of SingletonBag
-      in not used. Actually, we could just take as postulate:
-      [Parameter SingletonBag : A->multiset].  *)
-
-  #[deprecated(since="8.3", note="Use mergesort.v")]
-  Fixpoint contents (t:Tree) : multiset A :=
-    match t with
-      | Tree_Leaf => emptyBag
-      | Tree_Node a t1 t2 =>
-        munion (contents t1) (munion (contents t2) (singletonBag a))
-    end.
-
-
-  (** equivalence of two trees is equality of corresponding multisets *)
-  #[deprecated(since="8.3", note="Use mergesort.v")]
-  Definition equiv_Tree (t1 t2:Tree) := meq (contents t1) (contents t2).
-
-
-
-  (** * From lists to sorted lists *)
-
-  (** ** Specification of heap insertion *)
-
-  Inductive insert_spec (a:A) (T:Tree) : Type :=
-    insert_exist :
-    forall T1:Tree,
-      is_heap T1 ->
-      meq (contents T1) (munion (contents T) (singletonBag a)) ->
-      (forall b:A, leA b a -> leA_Tree b T -> leA_Tree b T1) ->
-      insert_spec a T.
-
-
-  #[deprecated(since="8.3", note="Use mergesort.v")]
-  Lemma insert : forall T:Tree, is_heap T -> forall a:A, insert_spec a T.
-  Proof.
-    simple induction 1; intros.
-    - apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf);
-        auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
-    - simpl; unfold meq, munion; auto using node_is_heap with datatypes.
-      elim (leA_dec a a0); intros.
-      + elim (X a0); intros.
-        apply insert_exist with (Tree_Node a T2 T0);
-          auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
-        simpl; apply treesort_twist1; trivial with datatypes.
-      + elim (X a); intros T3 HeapT3 ConT3 LeA.
-        apply insert_exist with (Tree_Node a0 T2 T3);
-          auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
-        * apply node_is_heap; auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
-          -- apply low_trans with a; auto with datatypes.
-          -- apply LeA; auto with datatypes.
-             apply low_trans with a; auto with datatypes.
-        * simpl; apply treesort_twist2; trivial with datatypes.
-  Qed.
-
-
-  (** ** Building a heap from a list *)
-
-  Inductive build_heap (l:list A) : Type :=
-    heap_exist :
-    forall T:Tree,
-      is_heap T ->
-      meq (list_contents _ eqA_dec l) (contents T) -> build_heap l.
-
-  #[deprecated(since="8.3", note="Use mergesort.v")]
-  Lemma list_to_heap : forall l:list A, build_heap l.
-  Proof.
-    simple induction l.
-    - apply (heap_exist nil Tree_Leaf); auto with datatypes.
-      simpl; unfold meq; exact nil_is_heap.
-    - simple induction 1.
-      intros T i m; elim (insert T i a).
-      intros; apply heap_exist with T1; simpl; auto with datatypes.
-      apply meq_trans with (munion (contents T) (singletonBag a)).
-      + apply meq_trans with (munion (singletonBag a) (contents T)).
-        * apply meq_right; trivial with datatypes.
-        * apply munion_comm.
-      + apply meq_sym; trivial with datatypes.
-  Qed.
-
-
-  (** ** Building the sorted list *)
-
-  Inductive flat_spec (T:Tree) : Type :=
-    flat_exist :
-    forall l:list A,
-      Sorted leA l ->
-      (forall a:A, leA_Tree a T -> HdRel leA a l) ->
-      meq (contents T) (list_contents _ eqA_dec l) -> flat_spec T.
-
-  #[deprecated(since="8.3", note="Use mergesort.v")]
-  Lemma heap_to_list : forall T:Tree, is_heap T -> flat_spec T.
-  Proof.
-    intros T h; elim h; intros.
-    - apply flat_exist with (nil (A:=A)); auto with datatypes.
-    - elim X; intros l1 s1 i1 m1; elim X0; intros l2 s2 i2 m2.
-      elim (merge _ s1 _ s2); intros.
-      apply flat_exist with (a :: l); simpl; auto with datatypes.
-      apply meq_trans with
-        (munion (list_contents _ eqA_dec l1)
-                (munion (list_contents _ eqA_dec l2) (singletonBag a))).
-      + apply meq_congr; auto with datatypes.
-      + apply meq_trans with
-          (munion (singletonBag a)
-                  (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2))).
-        * apply munion_rotate.
-        * apply meq_right; apply meq_sym; trivial with datatypes.
-  Qed.
-
-
-  (** * Specification of treesort *)
-
-  #[deprecated(since="8.3", note="Use mergesort.v")]
-  Theorem treesort :
-    forall l:list A,
-    {m : list A | Sorted leA m & permutation _ eqA_dec l m}.
-  Proof.
-    intro l; unfold permutation.
-    elim (list_to_heap l).
-    intros.
-    elim (heap_to_list T); auto with datatypes.
-    intros.
-    exists l0; auto with datatypes.
-    apply meq_trans with (contents T); trivial with datatypes.
-  Qed.
-
-End defs.
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v
deleted file mode 100644
index 239da46f14..0000000000
--- a/theories/Sorting/PermutEq.v
+++ /dev/null
@@ -1,231 +0,0 @@
-(************************************************************************)
-(*         *      The Rocq Prover / The Rocq Development Team           *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-From Stdlib Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation.
-
-Set Implicit Arguments.
-
-(** This file is similar to [PermutSetoid], except that the equality used here
-    is Coq usual one instead of a setoid equality. In particular, we can then
-    prove the equivalence between [Permutation.Permutation] and
-    [PermutSetoid.permutation].
-*)
-
-Section Perm.
-
-  Variable A : Type.
-  Hypothesis eq_dec : forall x y:A, {x=y} + {~ x=y}.
-
-  Notation permutation := (permutation _ eq_dec).
-  Notation list_contents := (list_contents _ eq_dec).
-
-  (** we can use [multiplicity] to define [In] and [NoDup]. *)
-
-  Lemma multiplicity_In :
-    forall l a, In a l <-> 0 < multiplicity (list_contents l) a.
-  Proof.
-    intros; split; intro H.
-    - eapply In_InA, multiplicity_InA in H; eauto with typeclass_instances.
-    - eapply multiplicity_InA, InA_alt in H as (y & -> & H); eauto with typeclass_instances.
-  Qed.
-
-  Lemma multiplicity_In_O :
-    forall l a, ~ In a l -> multiplicity (list_contents l) a = 0.
-  Proof.
-    intros l a; rewrite multiplicity_In;
-      destruct (multiplicity (list_contents l) a); auto.
-    destruct 1; auto with arith.
-  Qed.
-
-  Lemma multiplicity_In_S :
-    forall l a, In a l -> multiplicity (list_contents l) a >= 1.
-  Proof.
-    intros l a; rewrite multiplicity_In; auto.
-  Qed.
-
-  Lemma multiplicity_NoDup :
-    forall l, NoDup l <-> (forall a, multiplicity (list_contents l) a <= 1).
-  Proof.
-    induction l.
-    - simpl.
-      split; auto with arith.
-      intros; apply NoDup_nil.
-    - split; simpl.
-      + inversion_clear 1.
-        rewrite IHl in H1.
-        intros; destruct (eq_dec a a0) as [H2|H2]; simpl; auto.
-        subst a0.
-        rewrite multiplicity_In_O; auto.
-      + intros; constructor.
-        * rewrite multiplicity_In.
-          generalize (H a).
-          destruct (eq_dec a a) as [H0|H0].
-          -- destruct (multiplicity (list_contents l) a); auto with arith.
-             simpl; inversion 1.
-             inversion H3.
-          -- destruct H0; auto.
-        * rewrite IHl; intros.
-          generalize (H a0); auto with arith.
-          destruct (eq_dec a a0); simpl; auto with arith.
-  Qed.
-
-  Lemma NoDup_permut :
-    forall l l', NoDup l -> NoDup l' ->
-      (forall x, In x l <-> In x l') -> permutation l l'.
-  Proof.
-    intros.
-    red; unfold meq; intros.
-    rewrite multiplicity_NoDup in H, H0.
-    generalize (H a) (H0 a) (H1 a); clear H H0 H1.
-    do 2 rewrite multiplicity_In.
-    intros H H' [H0 H0'].
-    destruct (multiplicity (list_contents l) a) as [|[|n]],
-             (multiplicity (list_contents l') a) as [|[|n']];
-    [ tauto | | | | tauto | |  | | ]; try solve [intuition auto with arith]; exfalso.
-    - now inversion H'.
-    - now inversion H.
-    - now inversion H.
-  Qed.
-
-  (** Permutation is compatible with In. *)
-  Lemma permut_In_In :
-    forall l1 l2 e, permutation l1 l2 -> In e l1 -> In e l2.
-  Proof.
-    unfold PermutSetoid.permutation, meq; intros l1 l2 e P IN.
-    generalize (P e); clear P.
-    destruct (In_dec eq_dec e l2) as [H|H]; auto.
-    rewrite (multiplicity_In_O _ _ H).
-    intros.
-    generalize (multiplicity_In_S _ _ IN).
-    rewrite H0.
-    inversion 1.
-  Qed.
-
-  Lemma permut_cons_In :
-    forall l1 l2 e, permutation (e :: l1) l2 -> In e l2.
-  Proof.
-    intros; eapply permut_In_In; eauto.
-    red; auto.
-  Qed.
-
-  (** Permutation of an empty list. *)
-  Lemma permut_nil :
-    forall l, permutation l nil -> l = nil.
-  Proof.
-    intro l; destruct l as [ | e l ]; trivial.
-    assert (In e (e::l)) by (red; auto).
-    intro Abs; generalize (permut_In_In _ Abs H).
-    inversion 1.
-  Qed.
-
-  (** When used with [eq], this permutation notion is equivalent to
-      the one defined in [List.v]. *)
-
-  Lemma permutation_Permutation :
-    forall l l', Permutation l l' <-> permutation l l'.
-  Proof.
-    split.
-    - induction 1.
-      + apply permut_refl.
-      + apply permut_cons; auto.
-      + change (permutation (y::x::l) ((x::nil)++y::l)).
-        apply permut_add_cons_inside; simpl; apply permut_refl.
-      + apply permut_trans with l'; auto.
-    - revert l'.
-      induction l.
-      + intros.
-        rewrite (permut_nil (permut_sym H)).
-        apply Permutation_refl.
-      + intros.
-        destruct (In_split _ _ (permut_cons_In H)) as (h2,(t2,H1)).
-        subst l'.
-        apply Permutation_cons_app.
-        apply IHl.
-        apply permut_remove_hd with a; auto with typeclass_instances.
-  Qed.
-
-  (** Permutation for short lists. *)
-
-  Lemma permut_length_1:
-    forall a b, permutation (a :: nil) (b :: nil)  -> a=b.
-  Proof.
-    intros a b; unfold PermutSetoid.permutation, meq; intro P;
-      generalize (P b); clear P; simpl.
-    destruct (eq_dec b b) as [H|H]; [ | destruct H; auto].
-    destruct (eq_dec a b); simpl; auto; intros; discriminate.
-  Qed.
-
-  Lemma permut_length_2 :
-    forall a1 b1 a2 b2, permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) ->
-      (a1=a2) /\ (b1=b2) \/ (a1=b2) /\ (a2=b1).
-  Proof.
-    intros a1 b1 a2 b2 P.
-    assert (H:=permut_cons_In P).
-    inversion_clear H.
-    - left; split; auto.
-      apply permut_length_1.
-      red; red; intros.
-      generalize (P a); clear P; simpl.
-      destruct (eq_dec a1 a) as [H2|H2];
-        destruct (eq_dec a2 a) as [H3|H3]; auto.
-      + destruct H3; transitivity a1; auto.
-      + destruct H2; transitivity a2; auto.
-    - right.
-      inversion_clear H0; [|inversion H].
-      split; auto.
-      apply permut_length_1.
-      red; red; intros.
-      generalize (P a); clear P; simpl.
-      destruct (eq_dec a1 a) as [H2|H2];
-        destruct (eq_dec b2 a) as [H3|H3]; auto.
-      + simpl; rewrite <- plus_n_Sm; inversion 1; auto.
-      + destruct H3; transitivity a1; auto.
-      + destruct H2; transitivity b2; auto.
-  Qed.
-
-  (** Permutation is compatible with length. *)
-  Lemma permut_length :
-    forall l1 l2, permutation l1 l2 -> length l1 = length l2.
-  Proof.
-    induction l1; intros l2 H.
-    - rewrite (permut_nil (permut_sym H)); auto.
-    - destruct (In_split _ _ (permut_cons_In H)) as (h2,(t2,H1)).
-      subst l2.
-      rewrite length_app.
-      simpl; rewrite <- plus_n_Sm; f_equal.
-      rewrite <- length_app.
-      apply IHl1.
-      apply permut_remove_hd with a; auto with typeclass_instances.
-  Qed.
-
-  Variable B : Type.
-  Variable eqB_dec : forall x y:B, { x=y }+{ ~x=y }.
-
-  (** Permutation is compatible with map. *)
-
-  Lemma permutation_map :
-    forall f l1 l2, permutation l1 l2 ->
-      PermutSetoid.permutation _ eqB_dec (map f l1) (map f l2).
-  Proof.
-    intros f; induction l1.
-    - intros l2 P; rewrite (permut_nil (permut_sym P)); apply permut_refl.
-    - intros l2 P.
-      simpl.
-      destruct (In_split _ _ (permut_cons_In P)) as (h2,(t2,H1)).
-      subst l2.
-      rewrite map_app.
-      simpl.
-      apply permut_add_cons_inside.
-      rewrite <- map_app.
-      apply IHl1; auto.
-      apply permut_remove_hd with a; auto with typeclass_instances.
-  Qed.
-
-End Perm.
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
deleted file mode 100644
index 8897d6f5f9..0000000000
--- a/theories/Sorting/PermutSetoid.v
+++ /dev/null
@@ -1,546 +0,0 @@
-(************************************************************************)
-(*         *      The Rocq Prover / The Rocq Development Team           *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-From Stdlib Require Import Lia Relations Multiset SetoidList.
-
-(** This file is deprecated, use [Permutation.v] instead.
-
-    Indeed, this file defines a notion of permutation based on
-    multisets (there exists a permutation between two lists iff every
-    elements have the same multiplicity in the two lists) which
-    requires a more complex apparatus (the equipment of the domain
-    with a decidable equality) than [Permutation] in [Permutation.v].
-
-    The relation between the two relations are in lemma
-    [permutation_Permutation].
-
-    File [Permutation] concerns Leibniz equality : it shows in particular
-    that [List.Permutation] and [permutation] are equivalent in this context.
-*)
-
-Set Implicit Arguments.
-
-Local Notation "[ ]" := nil.
-Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).
-
-Section Permut.
-
-(** * From lists to multisets *)
-
-Variable A : Type.
-Variable eqA : relation A.
-Hypothesis eqA_equiv : Equivalence eqA.
-Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
-
-Let emptyBag := EmptyBag A.
-Let singletonBag := SingletonBag _ eqA_dec.
-
-(** contents of a list *)
-
-Fixpoint list_contents (l:list A) : multiset A :=
-  match l with
-  | [] => emptyBag
-  | a :: l => munion (singletonBag a) (list_contents l)
-  end.
-
-Lemma list_contents_app :
-  forall l m:list A,
-    meq (list_contents (l ++ m)) (munion (list_contents l) (list_contents m)).
-Proof.
-  simple induction l; simpl; auto with datatypes.
-  intros.
-  apply meq_trans with
-    (munion (singletonBag a) (munion (list_contents l0) (list_contents m)));
-    auto with datatypes.
-Qed.
-
-(** * [permutation]: definition and basic properties *)
-
-Definition permutation (l m:list A) := meq (list_contents l) (list_contents m).
-
-Lemma permut_refl : forall l:list A, permutation l l.
-Proof.
-  unfold permutation; auto with datatypes.
-Qed.
-
-Lemma permut_sym :
-  forall l1 l2 : list A, permutation l1 l2 -> permutation l2 l1.
-Proof.
-  unfold permutation, meq; intros; symmetry; trivial.
-Qed.
-
-Lemma permut_trans :
-  forall l m n:list A, permutation l m -> permutation m n -> permutation l n.
-Proof.
-  unfold permutation; intros.
-  apply meq_trans with (list_contents m); auto with datatypes.
-Qed.
-
-Lemma permut_cons_eq :
-  forall l m:list A,
-    permutation l m -> forall a a', eqA a a' -> permutation (a :: l) (a' :: m).
-Proof.
-  unfold permutation; simpl; intros.
-  apply meq_trans with (munion (singletonBag a') (list_contents l)).
-  - apply meq_left, meq_singleton; auto.
-  - auto with datatypes.
-Qed.
-
-Lemma permut_cons :
-  forall l m:list A,
-    permutation l m -> forall a:A, permutation (a :: l) (a :: m).
-Proof.
-  unfold permutation; simpl; auto with datatypes.
-Qed.
-
-Lemma permut_app :
-  forall l l' m m':list A,
-    permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m').
-Proof.
-  unfold permutation; intros.
-  apply meq_trans with (munion (list_contents l) (list_contents m));
-    auto using permut_cons, list_contents_app with datatypes.
-  apply meq_trans with (munion (list_contents l') (list_contents m'));
-    auto using permut_cons, list_contents_app with datatypes.
-  apply meq_trans with (munion (list_contents l') (list_contents m));
-    auto using permut_cons, list_contents_app with datatypes.
-Qed.
-
-Lemma permut_add_inside_eq :
-  forall a a' l1 l2 l3 l4, eqA a a' ->
-    permutation (l1 ++ l2) (l3 ++ l4) ->
-    permutation (l1 ++ a :: l2) (l3 ++ a' :: l4).
-Proof.
-  unfold permutation, meq in *; intros.
-  specialize H0 with a0.
-  repeat rewrite list_contents_app in *; simpl in *.
-  destruct (eqA_dec a a0) as [Ha|Ha]; rewrite H in Ha;
-    decide (eqA_dec a' a0) with Ha; simpl; auto with arith.
-  do 2 rewrite <- plus_n_Sm; f_equal; auto.
-Qed.
-
-Lemma permut_add_inside :
-  forall a l1 l2 l3 l4,
-    permutation (l1 ++ l2) (l3 ++ l4) ->
-    permutation (l1 ++ a :: l2) (l3 ++ a :: l4).
-Proof.
-  unfold permutation, meq in *; intros.
-  generalize (H a0); clear H.
-  do 4 rewrite list_contents_app.
-  simpl.
-  destruct (eqA_dec a a0); simpl; auto with arith.
-  do 2 rewrite <- plus_n_Sm; f_equal; auto.
-Qed.
-
-Lemma permut_add_cons_inside_eq :
-  forall a a' l l1 l2, eqA a a' ->
-    permutation l (l1 ++ l2) ->
-    permutation (a :: l) (l1 ++ a' :: l2).
-Proof.
-  intros;
-  replace (a :: l) with ([] ++ a :: l); trivial;
-    apply permut_add_inside_eq; trivial.
-Qed.
-
-Lemma permut_add_cons_inside :
-  forall a l l1 l2,
-    permutation l (l1 ++ l2) ->
-    permutation (a :: l) (l1 ++ a :: l2).
-Proof.
-  intros;
-    replace (a :: l) with ([] ++ a :: l); trivial;
-        apply permut_add_inside; trivial.
-Qed.
-
-Lemma permut_middle :
-  forall (l m:list A) (a:A), permutation (a :: l ++ m) (l ++ a :: m).
-Proof.
-  intros; apply permut_add_cons_inside; auto using permut_sym, permut_refl.
-Qed.
-
-Lemma permut_sym_app :
-  forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1).
-Proof.
-  intros l1 l2;
-    unfold permutation, meq;
-        intro a; do 2 rewrite list_contents_app; simpl;
-          auto with arith.
-Qed.
-
-Lemma permut_rev :
-  forall l, permutation l (rev l).
-Proof.
-  induction l.
-  - simpl; trivial using permut_refl.
-  - simpl.
-    apply permut_add_cons_inside.
-    rewrite app_nil_r. trivial.
-Qed.
-
-(** * Some inversion results. *)
-Lemma permut_conv_inv :
-  forall e l1 l2, permutation (e :: l1) (e :: l2) -> permutation l1 l2.
-Proof.
-  intros e l1 l2; unfold permutation, meq; simpl; intros H a;
-    generalize (H a); lia.
-Qed.
-
-Lemma permut_app_inv1 :
-  forall l l1 l2, permutation (l1 ++ l) (l2 ++ l) -> permutation l1 l2.
-Proof.
-  intros l l1 l2; unfold permutation, meq; simpl;
-    intros H a; generalize (H a); clear H.
-  do 2 rewrite list_contents_app.
-  simpl.
-  lia.
-Qed.
-
-(** we can use [multiplicity] to define [InA] and [NoDupA]. *)
-
-Fact if_eqA_then : forall a a' (B:Type)(b b':B),
- eqA a a' -> (if eqA_dec a a' then b else b') = b.
-Proof.
-  intros. destruct eqA_dec as [_|NEQ]; auto.
-  contradict NEQ; auto.
-Qed.
-
-Lemma permut_app_inv2 :
-  forall l l1 l2, permutation (l ++ l1) (l ++ l2) -> permutation l1 l2.
-Proof.
-  intros l l1 l2; unfold permutation, meq; simpl;
-    intros H a; generalize (H a); clear H.
-  do 2 rewrite list_contents_app.
-  simpl.
-  lia.
-Qed.
-
-Lemma permut_remove_hd_eq :
-  forall l l1 l2 a b, eqA a b ->
-    permutation (a :: l) (l1 ++ b :: l2) -> permutation l (l1 ++ l2).
-Proof.
-  unfold permutation, meq; simpl; intros l l1 l2 a b Heq H a0.
-  specialize H with a0.
-  rewrite list_contents_app in *. simpl in *.
-  destruct (eqA_dec a _) as [Ha|Ha]; rewrite Heq in Ha; revert H;
-    decide (eqA_dec b a0) with Ha; lia.
-Qed.
-
-Lemma permut_remove_hd :
-  forall l l1 l2 a,
-    permutation (a :: l) (l1 ++ a :: l2) -> permutation l (l1 ++ l2).
-Proof.
-  pose proof (Equivalence_Reflexive (R := eqA));
-  eauto using permut_remove_hd_eq.
-Qed.
-
-Fact if_eqA_else : forall a a' (B:Type)(b b':B),
- ~eqA a a' -> (if eqA_dec a a' then b else b') = b'.
-Proof.
-  intros. decide (eqA_dec a a') with H; auto.
-Qed.
-
-Fact if_eqA_refl : forall a (B:Type)(b b':B),
- (if eqA_dec a a then b else b') = b.
-Proof.
-  intros; apply (decide_left (eqA_dec a a)); auto with *.
-Qed.
-
-(** PL: Inutilisable dans un rewrite sans un change prealable. *)
-
-Global Instance if_eqA (B:Type)(b b':B) :
- Proper (eqA==>eqA==>@eq _) (fun x y => if eqA_dec x y then b else b').
-Proof.
- intros x x' Hxx' y y' Hyy'.
- intros; destruct (eqA_dec x y) as [H|H];
-  destruct (eqA_dec x' y') as [H'|H']; auto.
- - contradict H'; transitivity x; auto with *; transitivity y; auto with *.
- - contradict H; transitivity x'; auto with *; transitivity y'; auto with *.
-Qed.
-
-Fact if_eqA_rewrite_l : forall a1 a1' a2 (B:Type)(b b':B),
- eqA a1 a1' -> (if eqA_dec a1 a2 then b else b') =
-               (if eqA_dec a1' a2 then b else b').
-Proof.
- intros; destruct (eqA_dec a1 a2) as [A1|A1];
-  destruct (eqA_dec a1' a2) as [A1'|A1']; auto.
- - contradict A1'; transitivity a1; eauto with *.
- - contradict A1; transitivity a1'; eauto with *.
-Qed.
-
-Fact if_eqA_rewrite_r : forall a1 a2 a2' (B:Type)(b b':B),
- eqA a2 a2' -> (if eqA_dec a1 a2 then b else b') =
-               (if eqA_dec a1 a2' then b else b').
-Proof.
- intros; destruct (eqA_dec a1 a2) as [A2|A2];
-  destruct (eqA_dec a1 a2') as [A2'|A2']; auto.
- - contradict A2'; transitivity a2; eauto with *.
- - contradict A2; transitivity a2'; eauto with *.
-Qed.
-
-
-Global Instance multiplicity_eqA (l:list A) :
- Proper (eqA==>@eq _) (multiplicity (list_contents l)).
-Proof.
-  intros x x' Hxx'.
-  induction l as [|y l Hl]; simpl; auto.
-  rewrite (@if_eqA_rewrite_r y x x'); auto.
-Qed.
-
-Lemma multiplicity_InA :
-  forall l a, InA eqA a l <-> 0 < multiplicity (list_contents l) a.
-Proof.
-  induction l.
-  - simpl.
-    split; inversion 1.
-  - simpl.
-    intros a'; split; intros H.
-    + inversion_clear H.
-      * apply (decide_left (eqA_dec a a')); auto with *.
-      * destruct (eqA_dec a a'); auto with *. simpl; rewrite <- IHl; auto.
-    + destruct (eqA_dec a a'); auto with *. right. rewrite IHl; auto.
-Qed.
-
-Lemma multiplicity_InA_O :
-  forall l a, ~ InA eqA a l -> multiplicity (list_contents l) a = 0.
-Proof.
-  intros l a; rewrite multiplicity_InA;
-    destruct (multiplicity (list_contents l) a); auto with arith.
-  destruct 1; auto with arith.
-Qed.
-
-Lemma multiplicity_InA_S :
-  forall l a, InA eqA a l -> multiplicity (list_contents l) a >= 1.
-Proof.
-  intros l a; rewrite multiplicity_InA; auto with arith.
-Qed.
-
-Lemma multiplicity_NoDupA : forall l,
-  NoDupA eqA l <-> (forall a, multiplicity (list_contents l) a <= 1).
-Proof.
-  induction l.
-  - simpl.
-    split; auto with arith.
-  - split; simpl.
-    + inversion_clear 1.
-      rewrite IHl in H1.
-      intros; destruct (eqA_dec a a0) as [EQ|NEQ]; simpl; auto with *.
-      rewrite <- EQ.
-      rewrite multiplicity_InA_O; auto.
-    + intros; constructor.
-      * rewrite multiplicity_InA.
-        specialize (H a).
-        rewrite if_eqA_refl in H.
-        clear IHl; lia.
-      * rewrite IHl; intros.
-        specialize (H a0). lia.
-Qed.
-
-(** Permutation is compatible with InA. *)
-Lemma permut_InA_InA :
-  forall l1 l2 e, permutation l1 l2 -> InA eqA e l1 -> InA eqA e l2.
-Proof.
-  intros l1 l2 e.
-  do 2 rewrite multiplicity_InA.
-  unfold permutation, meq.
-  intros H;rewrite H; auto.
-Qed.
-
-Lemma permut_cons_InA :
-  forall l1 l2 e, permutation (e :: l1) l2 -> InA eqA e l2.
-Proof.
-  intros; apply (permut_InA_InA (e:=e) H); auto with *.
-Qed.
-
-(** Permutation of an empty list. *)
-Lemma permut_nil :
-  forall l, permutation l [] -> l = [].
-Proof.
-  intro l; destruct l as [ | e l ]; trivial.
-  assert (InA eqA e (e::l)) by (auto with *).
-  intro Abs; generalize (permut_InA_InA Abs H).
-  inversion 1.
-Qed.
-
-(** Permutation for short lists. *)
-
-Lemma permut_length_1:
-  forall a b, permutation [a] [b] -> eqA a b.
-Proof.
-  intros a b; unfold permutation, meq.
-  intro P; specialize (P b); simpl in *.
-  rewrite if_eqA_refl in *.
-  destruct (eqA_dec a b); simpl; auto; discriminate.
-Qed.
-
-Lemma permut_length_2 :
-  forall a1 b1 a2 b2, permutation [a1; b1] [a2; b2] ->
-    (eqA a1 a2) /\ (eqA b1 b2) \/ (eqA a1 b2) /\ (eqA a2 b1).
-Proof.
-  intros a1 b1 a2 b2 P.
-  assert (H:=permut_cons_InA P).
-  inversion_clear H.
-  - left; split; auto.
-    apply permut_length_1.
-    red; red; intros.
-    specialize (P a). simpl in *.
-    rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto. lia.
-  - right.
-    inversion_clear H0; [|inversion H].
-    split; auto.
-    apply permut_length_1.
-    red; red; intros.
-    specialize (P a); simpl in *.
-    rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto. lia.
-Qed.
-
-(** Permutation is compatible with length. *)
-Lemma permut_length :
-  forall l1 l2, permutation l1 l2 -> length l1 = length l2.
-Proof.
-  induction l1; intros l2 H.
-  - rewrite (permut_nil (permut_sym H)); auto.
-  - assert (H0:=permut_cons_InA H).
-    destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
-    subst l2.
-    rewrite length_app.
-    simpl; rewrite <- plus_n_Sm; f_equal.
-    rewrite <- length_app.
-    apply IHl1.
-    apply permut_remove_hd with b.
-    apply permut_trans with (a::l1); auto.
-    revert H1; unfold permutation, meq; simpl.
-    intros; f_equal; auto.
-    rewrite (@if_eqA_rewrite_l a b a0); auto.
-Qed.
-
-Lemma NoDupA_equivlistA_permut :
-  forall l l', NoDupA eqA l -> NoDupA eqA l' ->
-    equivlistA eqA l l' -> permutation l l'.
-Proof.
-  intros.
-  red; unfold meq; intros.
-  rewrite multiplicity_NoDupA in H, H0.
-  generalize (H a) (H0 a) (H1 a); clear H H0 H1.
-  do 2 rewrite multiplicity_InA.
-  destruct 3; lia.
-Qed.
-
-End Permut.
-
-Section Permut_map.
-
-Variables A B : Type.
-
-Variable eqA : relation A.
-Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
-Hypothesis eqA_equiv : Equivalence eqA.
-
-Variable eqB : B->B->Prop.
-Hypothesis eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }.
-Hypothesis eqB_trans : Transitive eqB.
-
-(** Permutation is compatible with map. *)
-
-Lemma permut_map :
-  forall f,
-    (Proper (eqA==>eqB) f) ->
-    forall l1 l2, permutation _ eqA_dec l1 l2 ->
-      permutation _ eqB_dec (map f l1) (map f l2).
-Proof.
-  intros f; induction l1.
-  - intros l2 P; rewrite (permut_nil eqA_equiv (permut_sym P)); apply permut_refl.
-  - intros l2 P.
-    simpl.
-    assert (H0:=permut_cons_InA eqA_equiv P).
-    destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
-    subst l2.
-    rewrite map_app.
-    simpl.
-    apply permut_trans with (f b :: map f l1).
-    + revert H1; unfold permutation, meq; simpl.
-      intros; f_equal; auto.
-      destruct (eqB_dec (f b) a0) as [H2|H2];
-        destruct (eqB_dec (f a) a0) as [H3|H3]; auto.
-      * destruct H3; transitivity (f b); auto with *.
-      * destruct H2; transitivity (f a); auto with *.
-    + apply permut_add_cons_inside.
-      rewrite <- map_app.
-      apply IHl1; auto.
-      apply permut_remove_hd with b; trivial.
-      apply permut_trans with (a::l1); auto.
-      revert H1; unfold permutation, meq; simpl.
-      intros; f_equal; auto.
-      rewrite (@if_eqA_rewrite_l _ _ eqA_equiv eqA_dec a b a0); auto.
-Qed.
-
-End Permut_map.
-
-From Stdlib Require Import Permutation.
-
-Section Permut_permut.
-
-Variable A : Type.
-
-Variable eqA : relation A.
-Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
-Hypothesis eqA_equiv : Equivalence eqA.
-
-Lemma Permutation_impl_permutation : forall l l',
-  Permutation l l' -> permutation _ eqA_dec l l'.
-Proof.
-  induction 1.
-  - apply permut_refl.
-  - apply permut_cons; auto using Equivalence_Reflexive.
-  - change (x :: y :: l) with ([x] ++ y :: l);
-      apply permut_add_cons_inside; simpl;
-      apply permut_cons_eq;
-      pose proof (Equivalence_Reflexive (R := eqA));
-      auto using permut_refl.
-  - apply permut_trans with l'; trivial.
-Qed.
-
-Lemma permut_eqA : forall l l', Forall2 eqA l l' -> permutation _ eqA_dec l l'.
-Proof.
-  induction 1.
-  - apply permut_refl.
-  - apply permut_cons_eq; trivial.
-Qed.
-
-Lemma permutation_Permutation : forall l l',
-  permutation _ eqA_dec l l' <->
-  exists l'', Permutation l l'' /\ Forall2 eqA l'' l'.
-Proof.
-  split; intro H.
-  - (* -> *)
-    induction l in l', H |- *.
-    + exists []; apply permut_sym, permut_nil in H as ->; auto using Forall2.
-    + pose proof H as H'.
-      apply permut_cons_InA, InA_split in H
-          as (l1 & y & l2 & Heq & ->); trivial.
-      apply permut_remove_hd_eq, IHl in H'
-          as (l'' & IHP & IHA); clear IHl; trivial.
-      apply Forall2_app_inv_r in IHA as (l1'' & l2'' & Hl1 & Hl2 & ->).
-      exists (l1'' ++ a :: l2''); split.
-      * apply Permutation_cons_app; trivial.
-      * apply Forall2_app, Forall2_cons; trivial.
-  - (* <- *)
-    destruct H as (l'' & H & Heq).
-    apply permut_trans with l''.
-    + apply Permutation_impl_permutation; trivial.
-    + apply permut_eqA; trivial.
-Qed.
-
-End Permut_permut.
-
-(* begin hide *)
-(** For compatibility *)
-Notation permut_right := permut_cons (only parsing).
-Notation permut_tran := permut_trans (only parsing).
-(* end hide *)