From c434f701f6beac210b8ea715ce6fe8e7d3dae1d3 Mon Sep 17 00:00:00 2001
From: Florent Hivert <Florent.Hivert@lri.fr>
Date: Sun, 24 Dec 2023 00:32:45 +0100
Subject: [PATCH] Removed unused and redudant lemmas

---
 theories/Combi/partition.v      |  3 +--
 theories/SSRcomplements/tools.v | 27 ---------------------------
 2 files changed, 1 insertion(+), 29 deletions(-)

diff --git a/theories/Combi/partition.v b/theories/Combi/partition.v
index e9f05dd..1ce13f4 100644
--- a/theories/Combi/partition.v
+++ b/theories/Combi/partition.v
@@ -2695,8 +2695,7 @@ Lemma ex_setpart_shape (s : seq nat) (A : {set T}) :
 Proof using.
 elim: s A => [| i s IHs] A /=.
   move=> /esym/cards0_eq -> _; exists [::]; split => //.
-  apply/partition0P; apply/setP => x.
-  by rewrite !inE in_nil.
+  by rewrite partition_set0.
 rewrite inE eq_sym => Hi /norP [Bne0 /IHs{IHs} Hrec].
 have: i <= #|A| by rewrite -Hi; apply: leq_addr.
 move=> /ex_subset_card [B BsubA /eqP cardB]; subst i.
diff --git a/theories/SSRcomplements/tools.v b/theories/SSRcomplements/tools.v
index d4dde64..c988ff2 100644
--- a/theories/SSRcomplements/tools.v
+++ b/theories/SSRcomplements/tools.v
@@ -502,24 +502,6 @@ Variable op : Monoid.com_law 1.
 Local Notation "'*%M'" := op (at level 0).
 Local Notation "x * y" := (op x y).
 
-(** mathcomp version is restrcticted to [s == enum I] for [I : finType] *)
-Lemma partition_big I (s : seq I)
-      (J : finType) (P : pred I) (p : I -> J) (Q : pred J) F :
-  (forall i, P i -> Q (p i)) ->
-  \big[*%M/1]_(i <- s | P i) F i =
-  \big[*%M/1]_(j : J | Q j) \big[*%M/1]_(i <- s | (P i) && (p i == j)) F i.
-Proof.
-move=> Qp; transitivity (\big[*%M/1]_(i <- s | P i && Q (p i)) F i).
-  by apply: eq_bigl => i; case Pi: (P i); rewrite // Qp.
-have [n leQn] := ubnP #|Q|; elim: n => // n IHn in Q {Qp} leQn *.
-case: (pickP Q) => [j Qj | Q0]; last first.
-  by rewrite !big_pred0 // => i; rewrite Q0 andbF.
-rewrite (bigD1 j) // -IHn; last by rewrite ltnS (cardD1x Qj) add1n in leQn.
-rewrite (bigID (fun i => p i == j)); congr (_ * _); apply: eq_bigl => i.
-  by case: eqP => [-> | _]; rewrite !(Qj, simpm).
-by rewrite andbA.
-Qed.
-
 Lemma big_seq_sub (T : countType) (s : seq T) F :
   \big[op/idx]_(x : seq_sub s) F (ssval x) = \big[op/idx]_(x <- undup s) F x.
 Proof.
@@ -542,15 +524,6 @@ Section SetPartition.
 Variable T : finType.
 Implicit Types (X : {set T}) (P : {set {set T}}).
 
-Lemma partition0P P : reflect (P = set0) (partition P set0).
-Proof using.
-apply (iffP and3P) => [[/eqP Hcov _ H0] | ->].
-- case: (set_0Vmem P) => [// | [X HXP]].
-  exfalso; suff HX : X = set0 by subst X; rewrite HXP in H0.
-  by apply/eqP; rewrite -subset0; rewrite -Hcov (bigcup_max X).
-- by split; rewrite ?inE // /trivIset /cover !big_set0 ?cards0.
-Qed.
-
 Lemma triv_part P X : X \in P -> partition P X -> P = [set X].
 Proof using.
 move=> HXP /and3P [/eqP Hcov /trivIsetP /(_ X _ HXP) H H0].