From 5d7bd2ea2a0a28fb275da8ba2e2c0dc5a33d1034 Mon Sep 17 00:00:00 2001
From: Georges Gonthier
Date: Wed, 8 May 2019 09:43:34 +0200
Subject: refactor `seq` permutation theory

- Change the naming of permutation lemmas so they conform to a
consistent policy: `perm_eq` lemmas have a `perm_` (_not_ `perm_eq`)
prefix, or sometimes a `_perm` suffix for lemmas that _prove_ `perm_eq`
using a property when there is also a lemma _using_ `perm_eq` for the
same property. Lemmas that do not concern `perm_eq` do _not_ have
`perm` in their name.
- Change the definition of `permutations` for a time- and space-
back-to-front generation algorithm.
- Add frequency tally operations `tally`, `incr_tally`, `wf_tally` and
`tally_seq`, used by the improved `permutation` algorithm.
- add deprecated aliases for renamed lemmas
---
 CHANGELOG.md                             |  35 ++
 mathcomp/Make                            |   2 +
 mathcomp/_CoqProject                     |   1 +
 mathcomp/algebra/ssrnum.v                |   3 +-
 mathcomp/algebra/vector.v                |   6 +-
 mathcomp/character/classfun.v            |   4 +-
 mathcomp/character/inertia.v             |   6 +-
 mathcomp/character/vcharacter.v          |  10 +-
 mathcomp/field/algebraics_fundamentals.v |   4 +-
 mathcomp/field/finfield.v                |   4 +-
 mathcomp/field/galois.v                  |   4 +-
 mathcomp/fingroup/gproduct.v             |  14 +-
 mathcomp/fingroup/perm.v                 |  17 +-
 mathcomp/solvable/abelian.v              |  10 +-
 mathcomp/solvable/extremal.v             |   2 +-
 mathcomp/solvable/jordanholder.v         |  20 +-
 mathcomp/ssreflect/bigop.v               |  25 +-
 mathcomp/ssreflect/path.v                |  36 +-
 mathcomp/ssreflect/prime.v               |   8 +-
 mathcomp/ssreflect/seq.v                 | 597 +++++++++++++++++++++----------
 mathcomp/ssreflect/ssreflect.v           |   9 +
 21 files changed, 552 insertions(+), 265 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3361567..4a6b7f6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -16,16 +16,51 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   warning for `old_id`; `Import Deprecation.Silent` turns off those warnings,
   `Import Deprecation.Reject` raises errors instead of only warning.
 
+- `filter_nseq`, `count_nseq`, `mem_nseq`,
+  `rcons_inj`, `rcons_injl`, `rcons_injr`, `nthK`, `sumn_rot`.
+
+- some `perm_eq` lemmas: `perm_cat[lr]`, `perm_nilP`,
+  `perm_consP`, `perm_has`, `perm_flatten`, `perm_sumn`.
+
+- computing (efficiently) (item, multiplicity) tallies of sequences over an
+  `eqType`: `tally s`, `incr_tally bs x`, `bs \is a wf_tally`, `tally_seq bs`.
+
 ### Changed
 
 - definition of `PredType` which now takes only a `P -> pred T` function;
   definition of `simpl_rel` to improve simplification by `inE`. Both these
   changes will be in the Coq 8.11 SSReflect core library.
 
+- definition of `permutations s` now uses an optimal algorithm (in space _and_
+  time) to generate all permutations of s back-to-front, using `tally s`.
+
 ### Renamed
 
+- `perm_eqP` -> `permP` (`seq.permP` if `perm.v` is also imported)
+- `perm_eqlP` -> `permPl`
+- `perm_eqrP` -> `permPr`
+- `perm_eqlE` -> `permEl`
+- `perm_eq_refl` -> `perm_refl`
+- `perm_eq_sym` -> `perm_sym`
+- `perm_eq_trans` -> `perm_trans`
+- `perm_eq_size` -> `perm_size`
+- `perm_eq_mem` -> `perm_mem`
+- `perm_eq_uniq` -> perm_uniq`
+- `perm_eq_rev` -> `perm_rev`
+- `perm_eq_flatten` -> `perm_flatten`
+- `perm_eq_all` -> `perm_all`
+- `perm_eq_small` -> `perm_small_eq`
+- `perm_eq_nilP` -> `perm_nilP`
+- `perm_eq_consP` -> `perm_consP`
 - `leq_size_perm` -> `uniq_min_size` (permuting conclusions)
 - `perm_uniq` -> `eq_uniq` (permuting assumptions)
+  --> beware `perm_uniq` now means `perm_eq_uniq`
+- `uniq_perm_eq` -> `uniq_perm`
+- `perm_eq_iotaP` -> `perm_iotaP`
+- `perm_undup_count` -> `perm_count_undup`
+- `tuple_perm_eqP` -> `tuple_permP`
+- `eq_big_perm` -> `perm_big`
+- `perm_eq_abelian_type` -> `abelian_type_pgroup`
 
 ### Misc
 
diff --git a/mathcomp/Make b/mathcomp/Make
index 4becdcb..bbb6433 100644
--- a/mathcomp/Make
+++ b/mathcomp/Make
@@ -95,3 +95,5 @@ test_suite/hierarchy_test.v
 -arg -w -arg -projection-no-head-constant
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -notation-overridden
+-arg -w -arg -duplicate-clear
+-arg -w -arg -ambiguous-paths
diff --git a/mathcomp/_CoqProject b/mathcomp/_CoqProject
index 450e035..912cc1a 100644
--- a/mathcomp/_CoqProject
+++ b/mathcomp/_CoqProject
@@ -4,3 +4,4 @@
 -arg -w -arg -projection-no-head-constant
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -notation-overridden
+-arg -w -arg -duplicate-clear
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 97afdfb..12fcecb 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -4384,8 +4384,7 @@ have sz_p: size p = n.+1.
 pose r := sort argCle r0; have r_arg: sorted argCle r by apply: sort_sorted.
 have{Dp} Dp: p = \prod_(z <- r) ('X - z%:P).
   rewrite Dp lead_coefE sz_p coefB coefXn coefC -mulrb -mulrnA mulnb lt0n andNb.
-  rewrite subr0 eqxx scale1r; apply: eq_big_perm.
-  by rewrite perm_eq_sym perm_sort.
+  by rewrite subr0 eqxx scale1r; apply/esym/perm_big; rewrite perm_sort.
 have mem_rP z: (n > 0)%N -> reflect (z ^+ n = x) (z \in r).
   move=> n_gt0; rewrite -root_prod_XsubC -Dp rootE !hornerE hornerXn n_gt0.
   by rewrite subr_eq0; apply: eqP.
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index e73ca33..87ca0f4 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -1004,7 +1004,7 @@ Proof. by rewrite /free span_seq1 dim_vline; case: (~~ _). Qed.
  
 Lemma perm_free X Y : perm_eq X Y -> free X = free Y.
 Proof.
-by move=> eqX; rewrite /free (perm_eq_size eqX) (eq_span (perm_eq_mem eqX)).
+by move=> eqXY; rewrite /free (perm_size eqXY) (eq_span (perm_mem eqXY)).
 Qed.
 
 Lemma free_directv X : free X = (0 \notin X) && directv (\sum_(v <- X) <[v]>).
@@ -1061,7 +1061,7 @@ Proof. by rewrite cat_free => /and3P[]. Qed.
 
 Lemma filter_free p X : free X -> free (filter p X).
 Proof.
-rewrite -(perm_free (etrans (perm_filterC p X _) (perm_eq_refl X))).
+rewrite -(perm_free (etrans (perm_filterC p X _) (perm_refl X))).
 exact: catl_free.
 Qed.
 
@@ -1170,7 +1170,7 @@ Qed.
 Lemma perm_basis X Y U : perm_eq X Y -> basis_of U X = basis_of U Y.
 Proof.
 move=> eqXY; congr ((_ == _) && _); last exact: perm_free.
-by apply/eq_span; apply: perm_eq_mem.
+by apply/eq_span; apply: perm_mem.
 Qed.
 
 Lemma vbasisP U : basis_of U (vbasis U).
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 65167b5..c35cdd6 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -1173,7 +1173,7 @@ Qed.
 
 Lemma eq_orthonormal R S : perm_eq R S -> orthonormal R = orthonormal S.
 Proof.
-move=> eqRS; rewrite !orthonormalE (eq_all_r (perm_eq_mem eqRS)).
+move=> eqRS; rewrite !orthonormalE (eq_all_r (perm_mem eqRS)).
 by rewrite (eq_pairwise_orthogonal eqRS).
 Qed.
 
@@ -2413,7 +2413,7 @@ set Su := map _ S => sSuS freeS; have uniqS := free_uniq freeS.
 have uniqSu: uniq Su by rewrite (map_inj_uniq cfAut_inj).
 have{sSuS} sSuS: {subset Su <= S} by move=> _ /mapP[phi Sphi ->]; apply: sSuS.
 have [|_ eqSuS] := uniq_min_size uniqSu sSuS; first by rewrite size_map.
-by rewrite (perm_free (uniq_perm_eq uniqSu uniqS eqSuS)).
+by rewrite (perm_free (uniq_perm uniqSu uniqS eqSuS)).
 Qed.
 
 Lemma cfAut_on A phi : (phi^u \in 'CF(G, A)) = (phi \in 'CF(G, A)).
diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v
index 5350075..d3dfd38 100644
--- a/mathcomp/character/inertia.v
+++ b/mathcomp/character/inertia.v
@@ -465,14 +465,14 @@ Lemma im_cfclass_Iirr i :
   H <| G -> perm_eq [seq 'chi_j | j in cfclass_Iirr G i] ('chi_i ^: G)%CF.
 Proof.
 move=> nsHG; have UchiG := cfclass_uniq 'chi_i nsHG.
-apply: uniq_perm_eq; rewrite ?(map_inj_uniq irr_inj) ?enum_uniq // => phi.
+apply: uniq_perm; rewrite ?(map_inj_uniq irr_inj) ?enum_uniq // => phi.
 apply/imageP/idP=> [[j iGj ->] | /cfclassP[y]]; first by rewrite -cfclass_IirrE.
 by exists (conjg_Iirr i y); rewrite ?mem_imset ?conjg_IirrE.
 Qed.
 
 Lemma card_cfclass_Iirr i : H <| G -> #|cfclass_Iirr G i| = #|G : 'I_G['chi_i]|.
 Proof.
-move=> nsHG; rewrite -size_cfclass -(perm_eq_size (im_cfclass_Iirr i nsHG)).
+move=> nsHG; rewrite -size_cfclass -(perm_size (im_cfclass_Iirr i nsHG)).
 by rewrite size_map -cardE.
 Qed.
 
@@ -481,7 +481,7 @@ Lemma reindex_cfclass R idx (op : Monoid.com_law idx) (F : 'CF(H) -> R) i :
   \big[op/idx]_(chi <- ('chi_i ^: G)%CF) F chi
      = \big[op/idx]_(j | 'chi_j \in ('chi_i ^: G)%CF) F 'chi_j.
 Proof.
-move/im_cfclass_Iirr/(eq_big_perm _) <-; rewrite big_map big_filter /=.
+move/im_cfclass_Iirr/(perm_big _) <-; rewrite big_map big_filter /=.
 by apply: eq_bigl => j; rewrite cfclass_IirrE.
 Qed.
 
diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v
index 4212fbe..4a113b6 100644
--- a/mathcomp/character/vcharacter.v
+++ b/mathcomp/character/vcharacter.v
@@ -314,7 +314,7 @@ Lemma cfproj_sum_orthogonal P z phi :
     = if P phi then z phi * '[phi] else 0.
 Proof.
 move=> Sphi; have defS := perm_to_rem Sphi.
-rewrite cfdot_suml (eq_big_perm _ defS) big_cons /= cfdotZl Inu ?Z_S //.
+rewrite cfdot_suml (perm_big _ defS) big_cons /= cfdotZl Inu ?Z_S //.
 rewrite big1_seq ?addr0 // => xi; rewrite mem_rem_uniq ?inE //.
 by case/and3P=> _ neq_xi Sxi; rewrite cfdotZl Inu ?Z_S // dotSS ?mulr0.
 Qed.
@@ -412,15 +412,15 @@ Lemma vchar_orthonormalP S :
 Proof.
 move=> vcS; apply: (equivP orthonormalP).
 split=> [[uniqS oSS] | [I [b defS]]]; last first.
-  split=> [|xi1 xi2]; rewrite ?(perm_eq_mem defS).
-    rewrite (perm_eq_uniq defS) map_inj_uniq ?enum_uniq // => i j /eqP.
+  split=> [|xi1 xi2]; rewrite ?(perm_mem defS).
+    rewrite (perm_uniq defS) map_inj_uniq ?enum_uniq // => i j /eqP.
     by rewrite eq_signed_irr => /andP[_ /eqP].
   case/mapP=> [i _ ->] /mapP[j _ ->]; rewrite eq_signed_irr.
   rewrite cfdotZl cfdotZr rmorph_sign mulrA cfdot_irr -signr_addb mulr_natr.
   by rewrite mulrb andbC; case: eqP => //= ->; rewrite addbb eqxx.
 pose I := [set i | ('chi_i \in S) || (- 'chi_i \in S)].
 pose b i := - 'chi_i \in S; exists I, b.
-apply: uniq_perm_eq => // [|xi].
+apply: uniq_perm => // [|xi].
   rewrite map_inj_uniq ?enum_uniq // => i j /eqP.
   by rewrite eq_signed_irr => /andP[_ /eqP].
 apply/idP/mapP=> [Sxi | [i Ii ->{xi}]]; last first.
@@ -453,7 +453,7 @@ move=> Zphi phiN1.
 have: orthonormal phi by rewrite /orthonormal/= phiN1 eqxx.
 case/vchar_orthonormalP=> [xi /predU1P[->|] // | I [b def_phi]].
 have: phi \in (phi : seq _) := mem_head _ _.
-by rewrite (perm_eq_mem def_phi) => /mapP[i _ ->]; exists (b i), i.
+by rewrite (perm_mem def_phi) => /mapP[i _ ->]; exists (b i), i.
 Qed.
 
 Lemma zchar_small_norm phi n :
diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index 6a28884..2d576c4 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -240,8 +240,8 @@ without loss{nCq} qx0: q mon_q q_dv_p / root (q ^ FtoL) x.
 have /dvdp_prod_XsubC[m Dq]: q ^ FtoL %| p_ I by rewrite DpI dvdp_map.
 pose B := [set j in mask m (enum I)]; have{Dq} Dq: q ^ FtoL = p_ B.
   apply/eqP; rewrite -eqp_monic ?monic_map ?monic_prod_XsubC //.
-  congr (_ %= _): Dq; apply: eq_big_perm => //.
-  by rewrite uniq_perm_eq ?mask_uniq ?enum_uniq // => j; rewrite mem_enum inE.
+  congr (_ %= _): Dq; apply: perm_big => //.
+  by rewrite uniq_perm ?mask_uniq ?enum_uniq // => j; rewrite mem_enum inE.
 rewrite -!(size_map_poly FtoL) Dq -DpI (minI B) // -?Dq ?FpxF //.
 by apply/subsetP=> j; rewrite inE => /mem_mask; rewrite mem_enum.
 Qed.
diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v
index 00a7bad..cb499b3 100644
--- a/mathcomp/field/finfield.v
+++ b/mathcomp/field/finfield.v
@@ -651,10 +651,10 @@ have prod_aq m: m %| n -> \prod_(d < n.+1 | d %| m) aq d = (q ^ m - 1)%:R.
     by rewrite !hornerE hornerXn -natrX natrB ?expn_gt0 ?prime_gt0.
   rewrite (prod_cyclotomic (dvdn_prim_root z_prim m_dv_n)).
   have def_divm: perm_eq (divisors m) [seq d <- index_iota 0 n.+1 | d %| m].
-    rewrite uniq_perm_eq ?divisors_uniq ?filter_uniq ?iota_uniq // => d.
+    rewrite uniq_perm ?divisors_uniq ?filter_uniq ?iota_uniq // => d.
     rewrite -dvdn_divisors ?(dvdn_gt0 n_gt0) // mem_filter mem_iota ltnS /=.
     by apply/esym/andb_idr=> d_dv_m; rewrite dvdn_leq ?(dvdn_trans d_dv_m).
-  rewrite (eq_big_perm _ def_divm) big_filter big_mkord horner_prod.
+  rewrite (perm_big _ def_divm) big_filter big_mkord horner_prod.
   by apply: eq_bigr => d d_dv_m; rewrite -exprM muln_divA ?divnK.
 have /rpredBl<-: (aq n %| #|G|%:R)%C.
   rewrite oG -prod_aq // (bigD1 ord_max) //= dvdC_mulr //.
diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v
index ae54fa1..30bef47 100644
--- a/mathcomp/field/galois.v
+++ b/mathcomp/field/galois.v
@@ -1329,12 +1329,12 @@ rewrite -fixedKE; apply/polyOverP => i; apply/fixedFieldP=> [|x galEx].
   rewrite (polyOverP _) // big_map rpred_prod // => b _.
   by rewrite polyOverXsubC memv_gal.
 rewrite -coef_map rmorph_prod; congr (_ : {poly _})`_i.
-symmetry; rewrite (eq_big_perm (map x r)) /= ?(big_map x).
+symmetry; rewrite (perm_big (map x r)) /= ?(big_map x).
   by apply: eq_bigr => b _; rewrite rmorphB /= map_polyX map_polyC.
 have Uxr: uniq (map x r) by rewrite map_inj_uniq //; apply: fmorph_inj.
 have /uniq_min_size: {subset map x r <= r}.
   by rewrite -map_comp => _ /codomP[b ->] /=; rewrite -galM // r_xa ?groupM.
-by rewrite (size_map x) perm_eq_sym; case=> // _ /uniq_perm_eq->.
+by rewrite (size_map x) perm_sym; case=> // _ /uniq_perm->.
 Qed.
 
 Lemma mem_galTrace K E a : galois K E -> a \in E -> galTrace K E a \in K.
diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v
index 676daf0..853ffb6 100644
--- a/mathcomp/fingroup/gproduct.v
+++ b/mathcomp/fingroup/gproduct.v
@@ -614,19 +614,19 @@ Lemma perm_bigcprod (I : eqType) r1 r2 (A : I -> {set gT}) G x :
   \prod_(i <- r1) x i = \prod_(i <- r2) x i.
 Proof.
 elim: r1 r2 G => [|i r1 IHr] r2 G defG Ax eq_r12.
-  by rewrite perm_eq_sym in eq_r12; rewrite (perm_eq_small _ eq_r12) ?big_nil.
-have /rot_to[n r3 Dr2]: i \in r2 by rewrite -(perm_eq_mem eq_r12) mem_head.
+  by rewrite perm_sym in eq_r12; rewrite (perm_small_eq _ eq_r12) ?big_nil.
+have /rot_to[n r3 Dr2]: i \in r2 by rewrite -(perm_mem eq_r12) mem_head.
 transitivity (\prod_(j <- rot n r2) x j).
   rewrite Dr2 !big_cons in defG Ax *; have [[_ G1 _ defG1] _ _] := cprodP defG.
   rewrite (IHr r3 G1) //; first by case/allP/andP: Ax => _ /allP.
-  by rewrite -(perm_cons i) -Dr2 perm_eq_sym perm_rot perm_eq_sym.
+  by rewrite -(perm_cons i) -Dr2 perm_sym perm_rot perm_sym.
 rewrite -{-2}(cat_take_drop n r2) in eq_r12 *.
-rewrite (eq_big_perm _ eq_r12) !big_cat /= !(big_nth i) !big_mkord in defG *.
+rewrite (perm_big _ eq_r12) !big_cat /= !(big_nth i) !big_mkord in defG *.
 have /cprodP[[G1 G2 defG1 defG2] _ /centsP-> //] := defG.
   rewrite defG2 -(bigcprodW defG2) mem_prodg // => k _; apply: Ax.
-  by rewrite (perm_eq_mem eq_r12) mem_cat orbC mem_nth.
+  by rewrite (perm_mem eq_r12) mem_cat orbC mem_nth.
 rewrite defG1 -(bigcprodW defG1) mem_prodg // => k _; apply: Ax.
-by rewrite (perm_eq_mem eq_r12) mem_cat mem_nth.
+by rewrite (perm_mem eq_r12) mem_cat mem_nth.
 Qed.
 
 Lemma reindex_bigcprod (I J : finType) (h : J -> I) P (A : I -> {set gT}) G x :
@@ -637,7 +637,7 @@ Proof.
 case=> h1 hK h1K; rewrite -!(big_filter _ P) filter_index_enum => defG Ax.
 rewrite -(big_map h P x) -(big_filter _ P) filter_map filter_index_enum.
 apply: perm_bigcprod defG _ _ => [i|]; first by rewrite mem_enum => /Ax.
-apply: uniq_perm_eq (enum_uniq P) _ _ => [|i].
+apply: uniq_perm (enum_uniq P) _ _ => [|i].
   by apply/dinjectiveP; apply: (can_in_inj hK).
 rewrite mem_enum; apply/idP/imageP=> [Pi | [j Phj ->//]].
 by exists (h1 i); rewrite ?inE h1K.
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index 33bf82c..b610c36 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -294,22 +294,22 @@ Proof.
 by apply/permP => z; rewrite -(permKV s z) permJ; apply/inj_tperm/perm_inj.
 Qed.
 
-Lemma tuple_perm_eqP {T : eqType} {n} {s : seq T} {t : n.-tuple T} :
+Lemma tuple_permP {T : eqType} {n} {s : seq T} {t : n.-tuple T} :
   reflect (exists p : 'S_n, s = [tuple tnth t (p i) | i < n]) (perm_eq s t).
 Proof.
 apply: (iffP idP) => [|[p ->]]; last first.
   rewrite /= (map_comp (tnth t)) -{1}(map_tnth_enum t) perm_map //.
-  apply: uniq_perm_eq => [||i]; rewrite ?enum_uniq //.
+  apply: uniq_perm => [||i]; rewrite ?enum_uniq //.
     by apply/injectiveP; apply: perm_inj.
   by rewrite mem_enum -[i](permKV p) image_f.
 case: n => [|n] in t *; last have x0 := tnth t ord0.
-  rewrite tuple0 => /perm_eq_small-> //.
+  rewrite tuple0 => /perm_small_eq-> //.
   by exists 1; rewrite [mktuple _]tuple0.
-case/(perm_eq_iotaP x0); rewrite size_tuple => Is eqIst ->{s}.
-have uniqIs: uniq Is by rewrite (perm_eq_uniq eqIst) iota_uniq.
-have szIs: size Is == n.+1 by rewrite (perm_eq_size eqIst) !size_tuple.
+case/(perm_iotaP x0); rewrite size_tuple => Is eqIst ->{s}.
+have uniqIs: uniq Is by rewrite (perm_uniq eqIst) iota_uniq.
+have szIs: size Is == n.+1 by rewrite (perm_size eqIst) !size_tuple.
 have pP i : tnth (Tuple szIs) i < n.+1.
-  by rewrite -[_ < _](mem_iota 0) -(perm_eq_mem eqIst) mem_tnth.
+  by rewrite -[_ < _](mem_iota 0) -(perm_mem eqIst) mem_tnth.
 have inj_p: injective (fun i => Ordinal (pP i)).
   by apply/injectiveP/(@map_uniq _ _ val); rewrite -map_comp map_tnth_enum.
 exists (perm inj_p); rewrite -[Is]/(tval (Tuple szIs)); congr (tval _).
@@ -577,5 +577,6 @@ End LiftPerm.
 
 Prenex Implicits lift_perm lift_permK.
 
-
+Notation tuple_perm_eqP :=
+  (deprecate tuple_perm_eqP tuple_permP) (only parsing).
 
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v
index ad12189..a51cbf2 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -1713,11 +1713,11 @@ rewrite orderXdiv ?pfactor_dvdn ?leq_subr // -(dvdn_pmul2r m_gt0).
 by rewrite -expnS -subSn // subSS divnK pfactor_dvdn ?leq_subr.
 Qed.
 
-Lemma perm_eq_abelian_type p b G :
+Lemma abelian_type_pgroup p b G :
     p.-group G -> \big[dprod/1]_(x <- b) <[x]> = G -> 1 \notin b ->
-  perm_eq (map order b) (abelian_type G).
+  perm_eq (abelian_type G) (map order b).
 Proof.
-move: b => b1 pG defG1 ntb1.
+rewrite perm_sym; move: b => b1 pG defG1 ntb1.
 have cGG: abelian G.
   elim: (b1) {pG}G defG1 => [_ <-|x b IHb G]; first by rewrite big_nil abelian1.
   rewrite big_cons; case/dprodP=> [[_ H _ defH]] <-; rewrite defH => cxH _.
@@ -1992,8 +1992,8 @@ suffices def_atG: abelian_type K ++ abelian_type H =i abelian_type G.
   by rewrite size_abelian_type // -abelian_type_homocyclic.
 have [bK defK atK] := abelian_structure cKK.
 have [bH defH atH] := abelian_structure cHH.
-apply: perm_eq_mem; rewrite -atK -atH -map_cat.
-apply: (perm_eq_abelian_type pG); first by rewrite big_cat defK defH.
+apply/perm_mem; rewrite perm_sym -atK -atH -map_cat.
+apply: (abelian_type_pgroup pG); first by rewrite big_cat defK defH.
 have: all [pred m | m > 1] (map order (bK ++ bH)).
   by rewrite map_cat all_cat atK atH !abelian_type_gt1.
 by rewrite all_map (eq_all (@order_gt1 _)) all_predC has_pred1.
diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v
index 65c186a..d236575 100644
--- a/mathcomp/solvable/extremal.v
+++ b/mathcomp/solvable/extremal.v
@@ -2322,7 +2322,7 @@ have{defZN2} strZN2: \big[dprod/1]_(z <- [:: xpn3; y]) <[z]> = 'Z('Ohm_2(N)).
   by rewrite unlock /= dprodg1.
 rewrite -size_abelian_type ?center_abelian //.
 have pZN2: p.-group 'Z('Ohm_2(N)) by rewrite (pgroupS _ pN) // subIset ?Ohm_sub.
-rewrite -(perm_eq_size (perm_eq_abelian_type pZN2 strZN2 _)) //= !inE.
+rewrite (perm_size (abelian_type_pgroup pZN2 strZN2 _)) //= !inE.
 rewrite !(eq_sym 1) -!order_eq1 oy orderE oX2.
 by rewrite (eqn_exp2l 2 0) // (eqn_exp2l 1 0).
 Qed.
diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v
index 1a32bce..d191e20 100644
--- a/mathcomp/solvable/jordanholder.v
+++ b/mathcomp/solvable/jordanholder.v
@@ -179,9 +179,9 @@ elim: {G}#|G| {-2}G (leqnn #|G|) => [|n Hi] G cG in s1 s2 * => cs1 cs2.
 have [G1 | ntG] := boolP (G :==: 1).
   have -> : s1 = [::] by apply/eqP; rewrite -(trivg_comps cs1).
   have -> : s2 = [::] by apply/eqP; rewrite -(trivg_comps cs2).
-  by rewrite /= perm_eq_refl.
+  by rewrite /= perm_refl.
 have [sG | nsG] := boolP (simple G).
-  by rewrite (simple_compsP cs1 sG) (simple_compsP cs2 sG) perm_eq_refl.
+  by rewrite (simple_compsP cs1 sG) (simple_compsP cs2 sG) perm_refl.
 case es1: s1 cs1 => [|N1 st1] cs1.
   by move: (trivg_comps cs1); rewrite eqxx; move/negP:ntG.
 case es2: s2 cs2 => [|N2 st2] cs2 {s1 es1}.
@@ -228,9 +228,9 @@ have i3 : perm_eq fG1 fG2.
   rewrite (@perm_catCA _ [::_] [::_]) /mksrepr.
   rewrite (@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso1).
   rewrite -(@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso2).
-  exact: perm_eq_refl.
-apply: (perm_eq_trans i1); apply: (perm_eq_trans i3); rewrite perm_eq_sym.
-by apply: perm_eq_trans i2; apply: perm_eq_refl.
+  exact: perm_refl.
+apply: (perm_trans i1); apply: (perm_trans i3); rewrite perm_sym.
+by apply: perm_trans i2; apply: perm_refl.
 Qed.
 
 End CompositionSeries.
@@ -593,11 +593,11 @@ elim: {G} #|G| {-2}G (leqnn #|G|) => [|n Hi] G cG in s1 s2 * => hsD cs1 cs2.
 case/orP: (orbN (G :==: 1)) => [tG | ntG].
   have -> : s1 = [::] by apply/eqP; rewrite -(trivg_acomps cs1).
   have -> : s2 = [::] by apply/eqP; rewrite -(trivg_acomps cs2).
-  by rewrite /= perm_eq_refl.
+  by rewrite /= perm_refl.
 case/orP: (orbN (asimple to G))=> [sG | nsG].
   have -> : s1 = [:: 1%G ] by apply/(asimple_acompsP cs1).
   have -> : s2 = [:: 1%G ] by apply/(asimple_acompsP cs2).
-  by rewrite /= perm_eq_refl.
+  by rewrite /= perm_refl.
 case es1: s1 cs1 => [|N1 st1] cs1.
   by move: (trivg_comps cs1); rewrite eqxx; move/negP:ntG.
 case es2: s2 cs2 => [|N2 st2] cs2 {s1 es1}.
@@ -667,9 +667,9 @@ have i3 : perm_eq fG1 fG2.
   rewrite (@perm_catCA _ [::_] [::_]) /mksrepr.
   rewrite (@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso1).
   rewrite -(@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso2).
-  exact: perm_eq_refl.
-apply: (perm_eq_trans i1); apply: (perm_eq_trans i3); rewrite perm_eq_sym.
-by apply: perm_eq_trans i2; apply: perm_eq_refl.
+  exact: perm_refl.
+apply: (perm_trans i1); apply: (perm_trans i3); rewrite perm_sym.
+by apply: perm_trans i2; apply: perm_refl.
 Qed.
 
 End StrongJordanHolder.
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 85fd47c..67e9c4b 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -1274,11 +1274,11 @@ Variable op : Monoid.com_law 1.
 Local Notation "'*%M'" := op (at level 0).
 Local Notation "x * y" := (op x y).
 
-Lemma eq_big_perm (I : eqType) r1 r2 (P : pred I) F :
+Lemma perm_big (I : eqType) r1 r2 (P : pred I) F :
     perm_eq r1 r2 ->
   \big[*%M/1]_(i <- r1 | P i) F i = \big[*%M/1]_(i <- r2 | P i) F i.
 Proof.
-move/perm_eqP; rewrite !(big_mkcond _ _ P).
+move/permP; rewrite !(big_mkcond _ _ P).
 elim: r1 r2 => [|i r1 IHr1] r2 eq_r12.
   by case: r2 eq_r12 => // i r2; move/(_ (pred1 i)); rewrite /= eqxx.
 have r2i: i \in r2 by rewrite -has_pred1 has_count -eq_r12 /= eqxx.
@@ -1290,8 +1290,8 @@ Qed.
 Lemma big_uniq (I : finType) (r : seq I) F :
   uniq r -> \big[*%M/1]_(i <- r) F i = \big[*%M/1]_(i in r) F i.
 Proof.
-move=> uniq_r; rewrite -(big_filter _ _ _ (mem r)); apply: eq_big_perm.
-by rewrite filter_index_enum uniq_perm_eq ?enum_uniq // => i; rewrite mem_enum.
+move=> uniq_r; rewrite -(big_filter _ _ _ (mem r)); apply: perm_big.
+by rewrite filter_index_enum uniq_perm ?enum_uniq // => i; rewrite mem_enum.
 Qed.
 
 Lemma big_rem (I : eqType) r x (P : pred I) F :
@@ -1299,7 +1299,7 @@ Lemma big_rem (I : eqType) r x (P : pred I) F :
   \big[*%M/1]_(y <- r | P y) F y
     = (if P x then F x else 1) * \big[*%M/1]_(y <- rem x r | P y) F y.
 Proof.
-by move/perm_to_rem/(eq_big_perm _)->; rewrite !(big_mkcond _ _ P) big_cons.
+by move/perm_to_rem/(perm_big _)->; rewrite !(big_mkcond _ _ P) big_cons.
 Qed.
 
 Lemma big_undup (I : eqType) (r : seq I) (P : pred I) F :
@@ -1316,15 +1316,15 @@ Lemma eq_big_idem (I : eqType) (r1 r2 : seq I) (P : pred I) F :
     idempotent *%M -> r1 =i r2 ->
   \big[*%M/1]_(i <- r1 | P i) F i = \big[*%M/1]_(i <- r2 | P i) F i.
 Proof.
-move=> idM eq_r; rewrite -big_undup // -(big_undup r2) //; apply/eq_big_perm.
-by rewrite uniq_perm_eq ?undup_uniq // => i; rewrite !mem_undup eq_r.
+move=> idM eq_r; rewrite -big_undup // -(big_undup r2) //; apply/perm_big.
+by rewrite uniq_perm ?undup_uniq // => i; rewrite !mem_undup eq_r.
 Qed.
 
 Lemma big_undup_iterop_count (I : eqType) (r : seq I) (P : pred I) F :
   \big[*%M/1]_(i <- undup r | P i) iterop (count_mem i r) *%M (F i) 1
     = \big[*%M/1]_(i <- r | P i) F i.
 Proof.
-rewrite -[RHS](eq_big_perm _ F (perm_undup_count _)) big_flatten big_map.
+rewrite -[RHS](perm_big _ F (perm_count_undup _)) big_flatten big_map.
 by rewrite big_mkcond; apply: eq_bigr => i _; rewrite big_nseq_cond iteropE.
 Qed.
 
@@ -1536,7 +1536,7 @@ Arguments big1_eq [R idx op I].
 Arguments big1_seq [R idx op I].
 Arguments big1 [R idx op I].
 Arguments big_pred1 [R idx op I] i [P F].
-Arguments eq_big_perm [R idx op I r1] r2 [P F].
+Arguments perm_big [R idx op I r1] r2 [P F].
 Arguments big_uniq [R idx op I] r [F].
 Arguments big_rem [R idx op I r] x [P F].
 Arguments bigID [R idx op I r].
@@ -1824,4 +1824,9 @@ Lemma biggcdn_inf (I : finType) i0 (P : pred I) F m :
 Proof. by move=> Pi0; apply: dvdn_trans; rewrite (bigD1 i0) ?dvdn_gcdl. Qed.
 Arguments biggcdn_inf [I] i0 [P F m].
 
-Unset Implicit Arguments.
+Notation "@ 'eq_big_perm'" :=
+  (deprecate eq_big_perm perm_big) (at level 10, only parsing).
+
+Notation eq_big_perm :=
+  ((fun R idx op I r1 P F r2 => @eq_big_perm R idx op I r1 r2 P F)
+        _   _  _ _  _ _ _) (only parsing).
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index 4d0d208..037adb8 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -430,13 +430,13 @@ Lemma eq_sorted : antisymmetric leT ->
   forall s1 s2, sorted s1 -> sorted s2 -> perm_eq s1 s2 -> s1 = s2.
 Proof.
 move=> leT_asym; elim=> [|x1 s1 IHs1] s2 //= ord_s1 ord_s2 eq_s12.
-  by case: {+}s2 (perm_eq_size eq_s12).
-have s2_x1: x1 \in s2 by rewrite -(perm_eq_mem eq_s12) mem_head.
+  by case: {+}s2 (perm_size eq_s12).
+have s2_x1: x1 \in s2 by rewrite -(perm_mem eq_s12) mem_head.
 case: s2 s2_x1 eq_s12 ord_s2 => //= x2 s2; rewrite in_cons.
 case: eqP => [<- _| ne_x12 /= s2_x1] eq_s12 ord_s2.
   by rewrite {IHs1}(IHs1 s2) ?(@path_sorted x1) // -(perm_cons x1).
 case: (ne_x12); apply: leT_asym; rewrite (allP (order_path_min ord_s2)) //.
-have: x2 \in x1 :: s1 by rewrite (perm_eq_mem eq_s12) mem_head.
+have: x2 \in x1 :: s1 by rewrite (perm_mem eq_s12) mem_head.
 case/predU1P=> [eq_x12 | s1_x2]; first by case ne_x12.
 by rewrite (allP (order_path_min ord_s1)).
 Qed.
@@ -447,7 +447,7 @@ Proof.
 move=> leT_irr s1 s2 s1_sort s2_sort eq_s12.
 have: antisymmetric leT.
   by move=> m n /andP[? ltnm]; case/idP: (leT_irr m); apply: leT_tr ltnm.
-by move/eq_sorted; apply=> //; apply: uniq_perm_eq => //; apply: sorted_uniq.
+by move/eq_sorted; apply=> //; apply: uniq_perm => //; apply: sorted_uniq.
 Qed.
 
 End Transitive.
@@ -482,20 +482,20 @@ Qed.
 
 Lemma perm_merge s1 s2 : perm_eql (merge s1 s2) (s1 ++ s2).
 Proof.
-apply/perm_eqlP; rewrite perm_eq_sym; elim: s1 s2 => //= x1 s1 IHs1.
+apply/permPl; rewrite perm_sym; elim: s1 s2 => //= x1 s1 IHs1.
 elim=> [|x2 s2 IHs2]; rewrite /= ?cats0 //.
 case: ifP => _ /=; last by rewrite perm_cons.
 by rewrite (perm_catCA (_ :: _) [::x2]) perm_cons.
 Qed.
 
 Lemma mem_merge s1 s2 : merge s1 s2 =i s1 ++ s2.
-Proof. by apply: perm_eq_mem; rewrite perm_merge. Qed.
+Proof. by apply: perm_mem; rewrite perm_merge. Qed.
 
 Lemma size_merge s1 s2 : size (merge s1 s2) = size (s1 ++ s2).
-Proof. by apply: perm_eq_size; rewrite perm_merge. Qed.
+Proof. by apply: perm_size; rewrite perm_merge. Qed.
 
 Lemma merge_uniq s1 s2 : uniq (merge s1 s2) = uniq (s1 ++ s2).
-Proof. by apply: perm_eq_uniq; rewrite perm_merge. Qed.
+Proof. by apply: perm_uniq; rewrite perm_merge. Qed.
 
 Fixpoint merge_sort_push s1 ss :=
   match ss with
@@ -531,30 +531,30 @@ Qed.
 
 Lemma perm_sort s : perm_eql (sort s) s.
 Proof.
-rewrite /sort; apply/perm_eqlP; pose catss := foldr (@cat T) [::].
-rewrite perm_eq_sym -{1}[s]/(catss [::] ++ s).
+rewrite /sort; apply/permPl; pose catss := foldr (@cat T) [::].
+rewrite perm_sym -{1}[s]/(catss [::] ++ s).
 elim: {s}_.+1 {-2}s [::] (ltnSn (size s)) => // n IHn s ss.
 have: perm_eq (catss ss ++ s) (merge_sort_pop s ss).
-  elim: ss s => //= s2 ss IHss s1; rewrite -{IHss}(perm_eqrP (IHss _)).
+  elim: ss s => //= s2 ss IHss s1; rewrite -{IHss}(permPr (IHss _)).
   by rewrite perm_catC catA perm_catC perm_cat2l -perm_merge.
 case: s => // x1 [//|x2 s _]; move/ltnW; move/IHn=> {n IHn}IHs.
-rewrite -{IHs}(perm_eqrP (IHs _)) ifE; set s1 := if_expr _ _ _.
+rewrite -{IHs}(permPr (IHs _)) ifE; set s1 := if_expr _ _ _.
 rewrite (catA _ [:: _; _] s) {s}perm_cat2r.
-apply: (@perm_eq_trans _ (catss ss ++ s1)).
+apply: (@perm_trans _ (catss ss ++ s1)).
   by rewrite perm_cat2l /s1 -ifE; case: ifP; rewrite // (perm_catC [:: _]).
 elim: ss {x1 x2}s1 => /= [|s2 ss IHss] s1; first by rewrite cats0.
 rewrite perm_catC; case def_s2: {2}s2=> /= [|y s2']; first by rewrite def_s2.
-by rewrite catA -{IHss}(perm_eqrP (IHss _)) perm_catC perm_cat2l -perm_merge.
+by rewrite catA -{IHss}(permPr (IHss _)) perm_catC perm_cat2l -perm_merge.
 Qed.
 
 Lemma mem_sort s : sort s =i s.
-Proof. by apply: perm_eq_mem; rewrite perm_sort. Qed.
+Proof. by apply: perm_mem; rewrite perm_sort. Qed.
 
 Lemma size_sort s : size (sort s) = size s.
-Proof. by apply: perm_eq_size; rewrite perm_sort. Qed.
+Proof. by apply: perm_size; rewrite perm_sort. Qed.
 
 Lemma sort_uniq s : uniq (sort s) = uniq s.
-Proof. by apply: perm_eq_uniq; rewrite perm_sort. Qed.
+Proof. by apply: perm_uniq; rewrite perm_sort. Qed.
 
 Lemma perm_sortP : transitive leT -> antisymmetric leT ->
   forall s1 s2, reflect (sort s1 = sort s2) (perm_eq s1 s2).
@@ -562,7 +562,7 @@ Proof.
 move=> leT_tr leT_asym s1 s2.
 apply: (iffP idP) => eq12; last by rewrite -perm_sort eq12 perm_sort.
 apply: eq_sorted; rewrite ?sort_sorted //.
-by rewrite perm_sort (perm_eqlP eq12) -perm_sort.
+by rewrite perm_sort (permPl eq12) -perm_sort.
 Qed.
 
 End SortSeq.
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index bcb163c..16e44e2 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -569,8 +569,8 @@ rewrite mem_seq1 mem_primes prime_gt0 //=.
 by apply/andP/idP=> [[pr_q q_p] | /eqP-> //]; rewrite -dvdn_prime2.
 Qed.
 
-Lemma coprime_has_primes m n : m > 0 -> n > 0 ->
-  coprime m n = ~~ has (mem (primes m)) (primes n).
+Lemma coprime_has_primes m n :
+  0 < m -> 0 < n -> coprime m n = ~~ has (mem (primes m)) (primes n).
 Proof.
 move=> m_gt0 n_gt0; apply/eqnP/hasPn=> [mn1 p | no_p_mn].
   rewrite /= !mem_primes m_gt0 n_gt0 /= => /andP[pr_p p_n].
@@ -1344,8 +1344,8 @@ Proof.
 move=> co_mn; have [-> //| m_gt0] := posnP m.
 have [->|n_gt0] := posnP n; first by rewrite !muln0.
 rewrite !totientE ?muln_gt0 ?m_gt0 //.
-have /(eq_big_perm _)->: perm_eq (primes (m * n)) (primes m ++ primes n).
-  apply: uniq_perm_eq => [||p]; first exact: primes_uniq.
+have /(perm_big _)->: perm_eq (primes (m * n)) (primes m ++ primes n).
+  apply: uniq_perm => [||p]; first exact: primes_uniq.
     by rewrite cat_uniq !primes_uniq -coprime_has_primes // co_mn.
   by rewrite mem_cat primes_mul.
 rewrite big_cat /= !big_seq.
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 76acaca..00e0a27 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -76,7 +76,15 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 (*        find p s == the index of the first item in s for which p holds,     *)
 (*                    or size s if no such item is found.                     *)
 (*       count p s == the number of items of s for which p holds.             *)
-(*   count_mem x s == the number of times x occurs in s := count (pred1 x) s. *)
+(*   count_mem x s == the multiplicity of x in s, i.e., count (pred1 x) s.    *)
+(*         tally s == a tally of s, i.e., a sequence of (item, multiplicity)  *)
+(*                    pairs for all items in sequence s (without duplicates). *)
+(* incr_tally bs x == increment the multiplicity of x in the tally bs, or add *)
+(*                    x with multiplicity 1 at then end if x is not in bs.    *)
+(* bs \is a wf_tally <=> bs is well-formed tally, with no duplicate items or  *)
+(*                    null multiplicities.                                    *)
+(*    tally_seq bs == the expansion of a tally bs into a sequence where each  *)
+(*                    (x, n) pair expands into a sequence of n x's.           *)
 (*      constant s <=> all items in s are identical (trivial if s = [::]).    *)
 (*          uniq s <=> all the items in s are pairwise different.             *)
 (*    subseq s1 s2 <=> s1 is a subsequence of s2, i.e., s1 = mask m s2 for    *)
@@ -84,11 +92,11 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 (*   perm_eq s1 s2 <=> s2 is a permutation of s1, i.e., s1 and s2 have the    *)
 (*                    items (with the same repetitions), but possibly in a    *)
 (*                    different order.                                        *)
-(*   permutations s == a duplicate-free list of all permutations of s.        *)
 (*  perm_eql s1 s2 <-> s1 and s2 behave identically on the left of perm_eq.   *)
 (*  perm_eqr s1 s2 <-> s1 and s2 behave identically on the right of perm_eq.  *)
 (* --> These left/right transitive versions of perm_eq make it easier to      *)
 (*  chain a sequence of equivalences.                                         *)
+(*   permutations s == a duplicate-free list of all permutations of s.        *)
 (*  ** Filtering:                                                             *)
 (*           filter p s == the subsequence of s consisting of all the items   *)
 (*                         for which the (boolean) predicate p holds.         *)
@@ -183,18 +191,16 @@ Open Scope seq_scope.
 
 (* Inductive seq (T : Type) : Type := Nil | Cons of T & seq T. *)
 Notation seq := list.
-Prenex Implicits cons.
+Bind Scope seq_scope with list.
+Arguments cons {T%type} x s%SEQ : rename.
+Arguments nil {T%type} : rename.
 Notation Cons T := (@cons T) (only parsing).
 Notation Nil T := (@nil T) (only parsing).
 
-Bind Scope seq_scope with list.
-Arguments cons _%type _ _%SEQ.
-
 (* As :: and ++ are (improperly) declared in Init.datatypes, we only rebind   *)
 (* them here.                                                                 *)
 Infix "::" := cons : seq_scope.
 
-(* GG - this triggers a camlp4 warning, as if this Notation had been Reserved *)
 Notation "[ :: ]" := nil (at level 0, format "[ :: ]") : seq_scope.
 
 Notation "[ :: x1 ]" := (x1 :: [::])
@@ -496,16 +502,20 @@ Proof. by elim: n => //= n ->; apply: orKb. Qed.
 Lemma all_nseqb (b : bool) x : all (nseq b x) = b ==> a x.
 Proof. by rewrite all_nseq eqb0 implybE. Qed.
 
+Lemma filter_nseq n x : filter (nseq n x) = nseq (a x * n) x.
+Proof. by elim: n => /= [|n ->]; case: (a x). Qed.
+
+Lemma count_nseq n x : count (nseq n x) = a x * n.
+Proof. by rewrite -size_filter filter_nseq size_nseq. Qed.
+
 Lemma find_nseq n x : find (nseq n x) = ~~ a x * n.
 Proof. by elim: n => /= [|n ->]; case: (a x). Qed.
 
 Lemma nth_find s : has s -> a (nth s (find s)).
-Proof. by elim: s => //= x s IHs; case Hx: (a x). Qed.
+Proof. by elim: s => //= x s IHs; case a_x: (a x). Qed.
 
 Lemma before_find s i : i < find s -> a (nth s i) = false.
-Proof.
-by elim: s i => //= x s IHs; case Hx: (a x) => [|] // [|i] //; apply: (IHs i).
-Qed.
+Proof. by elim: s i => //= x s IHs; case: ifP => // a'x [|i] // /(IHs i). Qed.
 
 Lemma filter_cat s1 s2 : filter (s1 ++ s2) = filter s1 ++ filter s2.
 Proof. by elim: s1 => //= x s1 ->; case (a x). Qed.
@@ -782,9 +792,6 @@ Qed.
 
 Lemma rot_inj : injective (rot n0). Proof. exact (can_inj rotK). Qed.
 
-Lemma rot1_cons x s : rot 1 (x :: s) = rcons s x.
-Proof. by rewrite /rot /= take0 drop0 -cats1. Qed.
-
 (* (efficient) reversal *)
 
 Fixpoint catrev s1 s2 := if s1 is x :: s1' then catrev s1' (x :: s2) else s2.
@@ -873,14 +880,37 @@ Proof.
 by move=> Pnil Pcons; elim=> [|x s IHs] [|y t] //= [eq_sz]; apply/Pcons/IHs.
 Qed.
 
+Section RotRcons.
+
+Variable T : Type.
+Implicit Types (x : T) (s : seq T).
+
+Lemma rot1_cons x s : rot 1 (x :: s) = rcons s x.
+Proof. by rewrite /rot /= take0 drop0 -cats1. Qed.
+
+Lemma rcons_inj s1 s2 x1 x2 :
+  rcons s1 x1 = rcons s2 x2 :> seq T -> (s1, x1) = (s2, x2).
+Proof. by rewrite -!rot1_cons => /rot_inj[-> ->]. Qed.
+
+Lemma rcons_injl x : injective (rcons^~ x).
+Proof. by move=> s1 s2 /rcons_inj[]. Qed.
+
+Lemma rcons_injr s : injective (rcons s).
+Proof. by move=> x1 x2 /rcons_inj[]. Qed.
+
+End RotRcons.
+
+Arguments rcons_inj {T s1 x1 s2 x2} eq_rcons : rename.
+Arguments rcons_injl {T} x [s1 s2] eq_rcons : rename.
+Arguments rcons_injr {T} s [x1 x2] eq_rcons : rename.
+
 (* Equality and eqType for seq.                                          *)
 
 Section EqSeq.
 
 Variables (n0 : nat) (T : eqType) (x0 : T).
 Local Notation nth := (nth x0).
-Implicit Type s : seq T.
-Implicit Types x y z : T.
+Implicit Types (x y z : T) (s : seq T).
 
 Fixpoint eqseq s1 s2 {struct s2} :=
   match s1, s2 with
@@ -1098,10 +1128,11 @@ Proof. by case: s => //= y s /andP[/eqP->]. Qed.
 Lemma all_pred1_nseq x n : all (pred1 x) (nseq n x).
 Proof. by rewrite all_nseq /= eqxx orbT. Qed.
 
+Lemma mem_nseq n x y : (y \in nseq n x) = (0 < n) && (y == x).
+Proof. by rewrite -has_pred1 has_nseq eq_sym.  Qed.
+
 Lemma nseqP n x y : reflect (y = x /\ n > 0) (y \in nseq n x).
-Proof.
-by rewrite -has_pred1 has_nseq /= eq_sym andbC; apply: (iffP andP) => -[/eqP].
-Qed.
+Proof. by rewrite mem_nseq andbC; apply: (iffP andP) => -[/eqP]. Qed.
 
 Lemma constant_nseq n x : constant (nseq n x).
 Proof. exact: all_pred1_constant (all_pred1_nseq x n). Qed.
@@ -1141,8 +1172,8 @@ Proof. by rewrite -cats1 uniq_catC. Qed.
 
 Lemma filter_uniq s a : uniq s -> uniq (filter a s).
 Proof.
-elim: s => [|x s IHs] //= /andP[Hx Hs]; case (a x); auto.
-by rewrite /= mem_filter /= (negbTE Hx) andbF; auto.
+elim: s => //= x s IHs /andP[s'x]; case: ifP => //= a_x /IHs->.
+by rewrite mem_filter a_x s'x.
 Qed.
 
 Lemma rot_uniq s : uniq (rot n0 s) = uniq s.
@@ -1180,7 +1211,7 @@ Proof. by elim: s => //= x s IHs; case: (x \in s) => //=; apply: ltnW. Qed.
 Lemma mem_undup s : undup s =i s.
 Proof.
 move=> x; elim: s => //= y s IHs.
-by case Hy: (y \in s); rewrite in_cons IHs //; case: eqP => // ->.
+by case s_y: (y \in s); rewrite !inE IHs //; case: eqP => [->|].
 Qed.
 
 Lemma undup_uniq s : uniq (undup s).
@@ -1193,7 +1224,7 @@ Proof. by elim: s => //= x s IHs /andP[/negbTE-> /IHs->]. Qed.
 
 Lemma ltn_size_undup s : (size (undup s) < size s) = ~~ uniq s.
 Proof.
-by elim: s => //= x s IHs; case Hx: (x \in s); rewrite //= ltnS size_undup.
+by elim: s => //= x s IHs; case s_x: (x \in s); rewrite //= ltnS size_undup.
 Qed.
 
 Lemma filter_undup p s : filter p (undup s) = undup (filter p s).
@@ -1222,13 +1253,15 @@ Lemma index_cat x s1 s2 :
  index x (s1 ++ s2) = if x \in s1 then index x s1 else size s1 + index x s2.
 Proof. by rewrite /index find_cat has_pred1. Qed.
 
-Lemma index_uniq i s : i < size s -> uniq s -> index (nth s i) s = i.
+Lemma nthK s: uniq s -> {in gtn (size s), cancel (nth s) (index^~ s)}.
 Proof.
-elim: s i => [|x s IHs] //= [|i]; rewrite /= ?eqxx // ltnS => lt_i_s.
-case/andP=> not_s_x /(IHs i)-> {IHs}//.
-by case: eqP not_s_x => // ->; rewrite mem_nth.
+elim: s => //= x s IHs /andP[s'x Us] i; rewrite inE ltnS eq_sym -if_neg.
+by case: i => /= [_|i lt_i_s]; rewrite ?eqxx ?IHs ?(memPn s'x) ?mem_nth.
 Qed.
 
+Lemma index_uniq i s : i < size s -> uniq s -> index (nth s i) s = i.
+Proof. by move/nthK. Qed.
+
 Lemma index_head x s : index x (x :: s) = 0.
 Proof. by rewrite /= eqxx. Qed.
 
@@ -1240,10 +1273,7 @@ Qed.
 
 Lemma nth_uniq s i j :
   i < size s -> j < size s -> uniq s -> (nth s i == nth s j) = (i == j).
-Proof.
-move=> lt_i_s lt_j_s Us; apply/eqP/eqP=> [eq_sij|-> //].
-by rewrite -(index_uniq lt_i_s Us) eq_sij index_uniq.
-Qed.
+Proof. by move=> lti ltj /nthK/can_in_eq->. Qed.
 
 Lemma uniqPn s :
   reflect (exists i j, [/\ i < j, j < size s & nth s i = nth s j]) (~~ uniq s).
@@ -1254,11 +1284,11 @@ elim: s => // x s IHs /nandP[/negbNE | /IHs[i [j]]]; last by exists i.+1, j.+1.
 by exists 0, (index x s).+1; rewrite !ltnS index_mem /= nth_index.
 Qed.
 
-Lemma uniqP s : reflect {in [pred i | i < size s] &, injective (nth s)} (uniq s).
+Lemma uniqP s : reflect {in gtn (size s) &, injective (nth s)} (uniq s).
 Proof.
-apply: (iffP idP) => [????? /eqP|]; first by rewrite nth_uniq // => /eqP.
-move=> nth_inj; apply/uniqPn => -[i [j [ltij ltjs /nth_inj ]]].
-by move=> /(_ (ltn_trans ltij ltjs)) /(_ ltjs) eq_ij; rewrite eq_ij ltnn in ltij.
+apply: (iffP idP) => [/nthK/can_in_inj// | nth_inj].
+apply/uniqPn => -[i [j [ltij ltjs /nth_inj/eqP/idPn]]].
+by rewrite !inE (ltn_trans ltij ltjs) ltn_eqF //=; case.
 Qed.
 
 Lemma mem_rot s : rot n0 s =i s.
@@ -1291,6 +1321,8 @@ Arguments allP {T a s}.
 Arguments allPn {T a s}.
 Arguments nseqP {T n x y}.
 Arguments count_memPn {T x s}.
+Arguments uniqPn {T} x0 {s}.
+Arguments uniqP {T} x0 {s}.
 
 Section NthTheory.
 
@@ -1379,7 +1411,7 @@ Implicit Type s : seq T.
 Definition perm_eq s1 s2 :=
   all [pred x | count_mem x s1 == count_mem x s2] (s1 ++ s2).
 
-Lemma perm_eqP s1 s2 : reflect (count^~ s1 =1 count^~ s2) (perm_eq s1 s2).
+Lemma permP s1 s2 : reflect (count^~ s1 =1 count^~ s2) (perm_eq s1 s2).
 Proof.
 apply: (iffP allP) => /= [eq_cnt1 a | eq_cnt x _]; last exact/eqP.
 elim: {a}_.+1 {-2}a (ltnSn (count a (s1 ++ s2))) => // n IHn a le_an.
@@ -1394,60 +1426,62 @@ apply: leq_trans le_an.
 by rewrite ltnS cnt_a' -add1n leq_add2r -has_count has_pred1.
 Qed.
 
-Lemma perm_eq_refl s : perm_eq s s.
-Proof. exact/perm_eqP. Qed.
-Hint Resolve perm_eq_refl : core.
+Lemma perm_refl s : perm_eq s s.
+Proof. exact/permP. Qed.
+Hint Resolve perm_refl : core.
 
-Lemma perm_eq_sym : symmetric perm_eq.
-Proof. by move=> s1 s2; apply/perm_eqP/perm_eqP=> ? ?. Qed.
+Lemma perm_sym : symmetric perm_eq.
+Proof. by move=> s1 s2; apply/permP/permP=> eq_s12 a. Qed.
 
-Lemma perm_eq_trans : transitive perm_eq.
-Proof. by move=> s2 s1 s3 /perm_eqP-eq12 /perm_eqP/(ftrans eq12)/perm_eqP. Qed.
+Lemma perm_trans : transitive perm_eq.
+Proof. by move=> s2 s1 s3 /permP-eq12 /permP/(ftrans eq12)/permP. Qed.
 
 Notation perm_eql s1 s2 := (perm_eq s1 =1 perm_eq s2).
 Notation perm_eqr s1 s2 := (perm_eq^~ s1 =1 perm_eq^~ s2).
 
-Lemma perm_eqlE s1 s2 : perm_eql s1 s2 -> perm_eq s1 s2. Proof. by move->. Qed.
+Lemma permEl s1 s2 : perm_eql s1 s2 -> perm_eq s1 s2. Proof. by move->. Qed.
 
-Lemma perm_eqlP s1 s2 : reflect (perm_eql s1 s2) (perm_eq s1 s2).
+Lemma permPl s1 s2 : reflect (perm_eql s1 s2) (perm_eq s1 s2).
 Proof.
-apply: (iffP idP) => [eq12 s3 | -> //].
-apply/idP/idP; last exact: perm_eq_trans.
-by rewrite -!(perm_eq_sym s3); move/perm_eq_trans; apply.
+apply: (iffP idP) => [eq12 s3 | -> //]; apply/idP/idP; last exact: perm_trans.
+by rewrite -!(perm_sym s3) => /perm_trans; apply.
 Qed.
 
-Lemma perm_eqrP s1 s2 : reflect (perm_eqr s1 s2) (perm_eq s1 s2).
+Lemma permPr s1 s2 : reflect (perm_eqr s1 s2) (perm_eq s1 s2).
 Proof.
-apply: (iffP idP) => [/perm_eqlP eq12 s3| <- //].
-by rewrite !(perm_eq_sym s3) eq12.
+by apply/(iffP idP) => [/permPl eq12 s3| <- //]; rewrite !(perm_sym s3) eq12.
 Qed.
 
 Lemma perm_catC s1 s2 : perm_eql (s1 ++ s2) (s2 ++ s1).
-Proof. by apply/perm_eqlP; apply/perm_eqP=> a; rewrite !count_cat addnC. Qed.
+Proof. by apply/permPl/permP=> a; rewrite !count_cat addnC. Qed.
 
 Lemma perm_cat2l s1 s2 s3 : perm_eq (s1 ++ s2) (s1 ++ s3) = perm_eq s2 s3.
 Proof.
-apply/perm_eqP/perm_eqP=> eq23 a; apply/eqP;
+apply/permP/permP=> eq23 a; apply/eqP;
   by move/(_ a)/eqP: eq23; rewrite !count_cat eqn_add2l.
 Qed.
 
-Lemma perm_catl s1 s2 s3 : perm_eq s2 s3 -> perm_eql (s1 ++ s2) (s1 ++ s3).
-Proof. by move=> eq_s23; apply/perm_eqlP; rewrite perm_cat2l. Qed.
+Lemma perm_catl s t1 t2 : perm_eq t1 t2 -> perm_eql (s ++ t1) (s ++ t2).
+Proof. by move=> eq_t12; apply/permPl; rewrite perm_cat2l. Qed.
 
 Lemma perm_cons x s1 s2 : perm_eq (x :: s1) (x :: s2) = perm_eq s1 s2.
 Proof. exact: (perm_cat2l [::x]). Qed.
 
 Lemma perm_cat2r s1 s2 s3 : perm_eq (s2 ++ s1) (s3 ++ s1) = perm_eq s2 s3.
-Proof. by do 2!rewrite perm_eq_sym perm_catC; apply: perm_cat2l. Qed.
+Proof. by do 2!rewrite perm_sym perm_catC; apply: perm_cat2l. Qed.
+
+Lemma perm_catr s1 s2 t : perm_eq s1 s2 -> perm_eql (s1 ++ t) (s2 ++ t).
+Proof. by move=> eq_s12; apply/permPl; rewrite perm_cat2r. Qed.
 
-Lemma perm_catr s1 s2 s3 : perm_eq s1 s2 -> perm_eql (s1 ++ s3) (s2 ++ s3).
-Proof. by move=> eq_s12; apply/perm_eqlP; rewrite perm_cat2r. Qed.
+Lemma perm_cat s1 s2 t1 t2 :
+  perm_eq s1 s2 -> perm_eq t1 t2 -> perm_eq (s1 ++ t1) (s2 ++ t2).
+Proof. by move=> /perm_catr-> /perm_catl->. Qed.
 
 Lemma perm_catAC s1 s2 s3 : perm_eql ((s1 ++ s2) ++ s3) ((s1 ++ s3) ++ s2).
-Proof. by apply/perm_eqlP; rewrite -!catA perm_cat2l perm_catC. Qed.
+Proof. by apply/permPl; rewrite -!catA perm_cat2l perm_catC. Qed.
 
 Lemma perm_catCA s1 s2 s3 : perm_eql (s1 ++ s2 ++ s3) (s2 ++ s1 ++ s3).
-Proof. by apply/perm_eqlP; rewrite !catA perm_cat2r perm_catC. Qed.
+Proof. by apply/permPl; rewrite !catA perm_cat2r perm_catC. Qed.
 
 Lemma perm_rcons x s : perm_eql (rcons s x) (x :: s).
 Proof. by move=> /= s2; rewrite -cats1 perm_catC. Qed.
@@ -1458,33 +1492,49 @@ Proof. by move=> /= s2; rewrite perm_catC cat_take_drop. Qed.
 Lemma perm_rotr n s : perm_eql (rotr n s) s.
 Proof. exact: perm_rot. Qed.
 
-Lemma perm_eq_rev s : perm_eq s (rev s).
-Proof. by apply/perm_eqP=> i; rewrite count_rev. Qed.
+Lemma perm_rev s : perm_eql (rev s) s.
+Proof. by apply/permPl/permP=> i; rewrite count_rev. Qed.
 
-Lemma perm_filter s1 s2 P :
-  perm_eq s1 s2 -> perm_eq (filter P s1) (filter P s2).
+Lemma perm_filter s1 s2 a :
+  perm_eq s1 s2 -> perm_eq (filter a s1) (filter a s2).
 Proof.
-by move/perm_eqP=> s12_count; apply/perm_eqP=> Q; rewrite !count_filter.
+by move/permP=> s12_count; apply/permP=> Q; rewrite !count_filter.
 Qed.
 
 Lemma perm_filterC a s : perm_eql (filter a s ++ filter (predC a) s) s.
 Proof.
-apply/perm_eqlP; elim: s => //= x s IHs.
+apply/permPl; elim: s => //= x s IHs.
 by case: (a x); last rewrite /= -cat1s perm_catCA; rewrite perm_cons.
 Qed.
 
-Lemma perm_eq_mem s1 s2 : perm_eq s1 s2 -> s1 =i s2.
-Proof. by move/perm_eqP=> eq12 x; rewrite -!has_pred1 !has_count eq12. Qed.
+Lemma perm_size s1 s2 : perm_eq s1 s2 -> size s1 = size s2.
+Proof. by move/permP=> eq12; rewrite -!count_predT eq12. Qed.
 
-Lemma perm_eq_all s1 s2 P : perm_eq s1 s2 -> all P s1 = all P s2.
-Proof. by move/perm_eq_mem/eq_all_r. Qed.
+Lemma perm_mem s1 s2 : perm_eq s1 s2 -> s1 =i s2.
+Proof. by move/permP=> eq12 x; rewrite -!has_pred1 !has_count eq12. Qed.
 
-Lemma perm_eq_size s1 s2 : perm_eq s1 s2 -> size s1 = size s2.
-Proof. by move/perm_eqP=> eq12; rewrite -!count_predT eq12. Qed.
+Lemma perm_nilP s : reflect (s = [::]) (perm_eq s [::]).
+Proof. by apply: (iffP idP) => [/perm_size/eqP/nilP | ->]. Qed.
 
-Lemma perm_eq_small s1 s2 : size s2 <= 1 -> perm_eq s1 s2 -> s1 = s2.
+Lemma perm_consP x s t :
+  reflect (exists i u, rot i t = x :: u /\ perm_eq u s)
+          (perm_eq t (x :: s)).
 Proof.
-move=> s2_le1 eqs12; move/perm_eq_size: eqs12 s2_le1 (perm_eq_mem eqs12).
+apply: (iffP idP) => [eq_txs | [i [u [Dt eq_us]]]].
+  have /rot_to[i u Dt]: x \in t by rewrite (perm_mem eq_txs) mem_head.
+  by exists i, u; rewrite -(perm_cons x) -Dt perm_rot.
+by rewrite -(perm_rot i) Dt perm_cons.
+Qed.
+
+Lemma perm_has s1 s2 a : perm_eq s1 s2 -> has a s1 = has a s2.
+Proof. by move/perm_mem/eq_has_r. Qed.
+
+Lemma perm_all s1 s2 a : perm_eq s1 s2 -> all a s1 = all a s2.
+Proof. by move/perm_mem/eq_all_r. Qed.
+
+Lemma perm_small_eq s1 s2 : size s2 <= 1 -> perm_eq s1 s2 -> s1 = s2.
+Proof.
+move=> s2_le1 eqs12; move/perm_size: eqs12 s2_le1 (perm_mem eqs12).
 by case: s2 s1 => [|x []] // [|y []] // _ _ /(_ x); rewrite !inE eqxx => /eqP->.
 Qed.
 
@@ -1533,35 +1583,25 @@ move=> eq_sz12 eq_s12.
 by apply/idP/idP=> Us; rewrite (uniq_size_uniq Us) ?eq_sz12 ?eqxx.
 Qed.
 
-Lemma perm_eq_uniq s1 s2 : perm_eq s1 s2 -> uniq s1 = uniq s2.
-Proof.
-by move=> eq_s12; apply/eq_uniq; [apply: perm_eq_size | apply: perm_eq_mem].
-Qed.
+Lemma perm_uniq s1 s2 : perm_eq s1 s2 -> uniq s1 = uniq s2.
+Proof. by move=> eq_s12; apply/eq_uniq; [apply/perm_size | apply/perm_mem]. Qed.
 
-Lemma uniq_perm_eq s1 s2 : uniq s1 -> uniq s2 -> s1 =i s2 -> perm_eq s1 s2.
+Lemma uniq_perm s1 s2 : uniq s1 -> uniq s2 -> s1 =i s2 -> perm_eq s1 s2.
 Proof.
 move=> Us1 Us2 eq12; apply/allP=> x _; apply/eqP.
 by rewrite !count_uniq_mem ?eq12.
 Qed.
 
-Lemma count_mem_uniq s : (forall x, count_mem x s = (x \in s)) -> uniq s.
+Lemma perm_undup s1 s2 : s1 =i s2 -> perm_eq (undup s1) (undup s2).
 Proof.
-move=> count1_s; have Uus := undup_uniq s.
-suffices: perm_eq s (undup s) by move/perm_eq_uniq->.
-by apply/allP=> x _; apply/eqP; rewrite (count_uniq_mem x Uus) mem_undup.
+by move=> Es12; rewrite uniq_perm ?undup_uniq // => s; rewrite !mem_undup.
 Qed.
 
-Lemma perm_eq_nilP s : reflect (s = [::]) (perm_eq s [::]).
-Proof. by case: s => [|x s]; rewrite /perm_eq /= ?eqxx; constructor. Qed.
-
-Lemma perm_eq_consP x s t :
-  reflect (exists i t1, rot i t = x :: t1 /\ perm_eq s t1)
-          (perm_eq (x :: s) t).
+Lemma count_mem_uniq s : (forall x, count_mem x s = (x \in s)) -> uniq s.
 Proof.
-rewrite perm_eq_sym; apply: (iffP idP) => [eq_ts | [i [t1 [Dt eq_st]]]].
-  have /rot_to[i t1 Dt]: x \in t by rewrite (perm_eq_mem eq_ts) mem_head.
-  by exists i, t1; rewrite -(perm_cons x) -Dt perm_eq_sym perm_rot.
-by rewrite -(perm_rot i) Dt perm_cons perm_eq_sym.
+move=> count1_s; have Uus := undup_uniq s.
+suffices: perm_eq s (undup s) by move/perm_uniq->.
+by apply/allP=> x _; apply/eqP; rewrite (count_uniq_mem x Uus) mem_undup.
 Qed.
 
 Lemma catCA_perm_ind P :
@@ -1570,8 +1610,8 @@ Lemma catCA_perm_ind P :
 Proof.
 move=> PcatCA s1 s2 eq_s12; rewrite -[s1]cats0 -[s2]cats0.
 elim: s2 nil => [|x s2 IHs] s3 in s1 eq_s12 *.
-  by case: s1 {eq_s12}(perm_eq_size eq_s12).
-have /rot_to[i s' def_s1]: x \in s1 by rewrite (perm_eq_mem eq_s12) mem_head.
+  by case: s1 {eq_s12}(perm_size eq_s12).
+have /rot_to[i s' def_s1]: x \in s1 by rewrite (perm_mem eq_s12) mem_head.
 rewrite -(cat_take_drop i s1) -catA => /PcatCA.
 rewrite catA -/(rot i s1) def_s1 /= -cat1s => /PcatCA/IHs/PcatCA; apply.
 by rewrite -(perm_cons x) -def_s1 perm_rot.
@@ -1590,16 +1630,16 @@ End PermSeq.
 Notation perm_eql s1 s2 := (perm_eq s1 =1 perm_eq s2).
 Notation perm_eqr s1 s2 := (perm_eq^~ s1 =1 perm_eq^~ s2).
 
-Arguments perm_eqP {T s1 s2}.
-Arguments perm_eqlP {T s1 s2}.
-Arguments perm_eqrP {T s1 s2}.
+Arguments permP {T s1 s2}.
+Arguments permPl {T s1 s2}.
+Arguments permPr {T s1 s2}.
 Prenex Implicits perm_eq.
-Hint Resolve perm_eq_refl : core.
+Hint Resolve perm_refl : core.
 
 Section RotrLemmas.
 
 Variables (n0 : nat) (T : Type) (T' : eqType).
-Implicit Type s : seq T.
+Implicit Types (x : T) (s : seq T).
 
 Lemma size_rotr s : size (rotr n0 s) = size s.
 Proof. by rewrite size_rot. Qed.
@@ -1908,13 +1948,13 @@ Qed.
 
 Lemma perm_to_rem s : x \in s -> perm_eq s (x :: rem s).
 Proof.
-elim: s => // y s IHs; rewrite inE /= eq_sym perm_eq_sym.
+elim: s => // y s IHs; rewrite inE /= eq_sym perm_sym.
 case: eqP => [-> // | _ /IHs].
-by rewrite (perm_catCA [:: x] [:: y]) perm_cons perm_eq_sym.
+by rewrite (perm_catCA [:: x] [:: y]) perm_cons perm_sym.
 Qed.
 
 Lemma size_rem s : x \in s -> size (rem s) = (size s).-1.
-Proof. by move/perm_to_rem/perm_eq_size->. Qed.
+Proof. by move/perm_to_rem/perm_size->. Qed.
 
 Lemma rem_subseq s : subseq (rem s) s.
 Proof.
@@ -2067,8 +2107,8 @@ Lemma subseq_uniqP s1 s2 :
 Proof.
 move=> uniq_s2; apply: (iffP idP) => [ss12 | ->]; last exact: filter_subseq.
 apply/eqP; rewrite -size_subseq_leqif ?subseq_filter ?(introT allP) //.
-apply/eqP/esym/perm_eq_size.
-rewrite uniq_perm_eq ?filter_uniq ?(subseq_uniq ss12) // => x.
+apply/eqP/esym/perm_size.
+rewrite uniq_perm ?filter_uniq ?(subseq_uniq ss12) // => x.
 by rewrite mem_filter; apply: andb_idr; apply: (mem_subseq ss12).
 Qed.
 
@@ -2093,18 +2133,14 @@ Implicit Type s : seq T1.
 
 Lemma map_f s x : x \in s -> f x \in map f s.
 Proof.
-elim: s => [|y s IHs] //=.
-by case/predU1P=> [->|Hx]; [apply: predU1l | apply: predU1r; auto].
+by elim: s => //= y s IHs /predU1P[->|/IHs]; [apply: predU1l | apply: predU1r].
 Qed.
 
 Lemma mapP s y : reflect (exists2 x, x \in s & y = f x) (y \in map f s).
 Proof.
-elim: s => [|x s IHs]; first by right; case.
-rewrite /= in_cons eq_sym; case Hxy: (f x == y).
-  by left; exists x; [rewrite mem_head | rewrite (eqP Hxy)].
-apply: (iffP IHs) => [[x' Hx' ->]|[x' Hx' Dy]].
-  by exists x'; first apply: predU1r.
-by move: Dy Hxy => ->; case/predU1P: Hx' => [->|]; [rewrite eqxx | exists x'].
+elim: s => [|x s IHs]; [by right; case | rewrite /= inE].
+have [Dy | fx'y] := y =P f x; first by left; exists x; rewrite ?mem_head.
+by apply: (iffP IHs) => [[z]|[z /predU1P[->|]]]; exists z; do ?apply: predU1r.
 Qed.
 
 Lemma map_uniq s : uniq (map f s) -> uniq s.
@@ -2136,7 +2172,7 @@ by apply: sub_in2 inj_f => z; apply: predU1r.
 Qed.
 
 Lemma perm_map s t : perm_eq s t -> perm_eq (map f s) (map f t).
-Proof. by move/perm_eqP=> Est; apply/perm_eqP=> a; rewrite !count_map Est. Qed.
+Proof. by move/permP=> Est; apply/permP=> a; rewrite !count_map Est. Qed.
 
 Hypothesis Hf : injective f.
 
@@ -2151,7 +2187,7 @@ Proof. by apply: map_inj_in_uniq; apply: in2W. Qed.
 
 Lemma perm_map_inj s t : perm_eq (map f s) (map f t) -> perm_eq s t.
 Proof.
-move/perm_eqP=> Est; apply/allP=> x _ /=.
+move/permP=> Est; apply/allP=> x _ /=.
 have Dx: pred1 x =1 preim f (pred1 (f x)) by move=> y /=; rewrite inj_eq.
 by rewrite !(eq_count Dx) -!count_map Est.
 Qed.
@@ -2342,14 +2378,14 @@ Variable T : eqType.
 Lemma mkseq_uniq (f : nat -> T) n : injective f -> uniq (mkseq f n).
 Proof. by move/map_inj_uniq->; apply: iota_uniq. Qed.
 
-Lemma perm_eq_iotaP {s t : seq T} x0 (It := iota 0 (size t)) :
+Lemma perm_iotaP {s t : seq T} x0 (It := iota 0 (size t)) :
   reflect (exists2 Is, perm_eq Is It & s = map (nth x0 t) Is) (perm_eq s t).
 Proof.
 apply: (iffP idP) => [Est | [Is eqIst ->]]; last first.
   by rewrite -{2}[t](mkseq_nth x0) perm_map.
 elim: t => [|x t IHt] in s It Est *.
-  by rewrite (perm_eq_small _ Est) //; exists [::].
-have /rot_to[k s1 Ds]: x \in s by rewrite (perm_eq_mem Est) mem_head.
+  by rewrite (perm_small_eq _ Est) //; exists [::].
+have /rot_to[k s1 Ds]: x \in s by rewrite (perm_mem Est) mem_head.
 have [|Is1 eqIst1 Ds1] := IHt s1; first by rewrite -(perm_cons x) -Ds perm_rot.
 exists (rotr k (0 :: map succn Is1)).
   by rewrite perm_rot /It /= perm_cons (iota_addl 1) perm_map.
@@ -2358,7 +2394,7 @@ Qed.
 
 End MakeEqSeq.
 
-Arguments perm_eq_iotaP {T s t}.
+Arguments perm_iotaP {T s t}.
 
 Section FoldRight.
 
@@ -2391,15 +2427,22 @@ Proof. by rewrite mulnC; elim: n => //= n ->. Qed.
 Lemma sumn_cat s1 s2 : sumn (s1 ++ s2) = sumn s1 + sumn s2.
 Proof. by elim: s1 => //= x s1 ->; rewrite addnA. Qed.
 
-Lemma sumn_count T (P : pred T) s :
-  sumn [seq (P i : nat) | i <- s] = count P s.
+Lemma sumn_count T (a : pred T) s : sumn [seq a i : nat | i <- s] = count a s.
 Proof. by elim: s => //= s0 s /= ->. Qed.
 
 Lemma sumn_rcons s n : sumn (rcons s n) = sumn s + n.
 Proof. by rewrite -cats1 sumn_cat /= addn0. Qed.
 
+Lemma perm_sumn s1 s2 : perm_eq s1 s2 -> sumn s1 = sumn s2.
+Proof.
+by apply/catCA_perm_subst: s1 s2 => s1 s2 s3; rewrite !sumn_cat addnCA.
+Qed.
+
+Lemma sumn_rot s n : sumn (rot n s) = sumn s.
+Proof. by apply/perm_sumn; rewrite perm_rot. Qed.
+
 Lemma sumn_rev s : sumn (rev s) = sumn s.
-Proof. by elim: s => //= x s <-; rewrite rev_cons sumn_rcons addnC. Qed.
+Proof. by apply/perm_sumn; rewrite perm_rev. Qed.
 
 Lemma natnseq0P s : reflect (s = nseq (size s) 0) (sumn s == 0).
 Proof.
@@ -2753,7 +2796,7 @@ Qed.
 Lemma perm_flatten (ss1 ss2 : seq (seq T)) :
   perm_eq ss1 ss2 -> perm_eq (flatten ss1) (flatten ss2).
 Proof.
-move=> eq_ss; apply/perm_eqP=> a; apply/catCA_perm_subst: ss1 ss2 eq_ss.
+move=> eq_ss; apply/permP=> a; apply/catCA_perm_subst: ss1 ss2 eq_ss.
 by move=> ss1 ss2 ss3; rewrite !flatten_cat !count_cat addnCA.
 Qed.
 
@@ -2762,20 +2805,6 @@ End EqFlatten.
 Arguments flattenP {T A x}.
 Arguments flatten_mapP {S T A s y}.
 
-Lemma perm_undup_count (T : eqType) (s : seq T) :
-  perm_eq (flatten [seq nseq (count_mem x s) x | x <- undup s]) s.
-Proof.
-pose N x r := count_mem x (flatten [seq nseq (count_mem y s) y | y <- r]).
-apply/allP=> x _; rewrite /= -/(N x _).
-have Nx0 r (r'x : x \notin r): N x r = 0.
-  by apply/count_memPn; apply: contra r'x => /flatten_mapP[y r_y /nseqP[->]].
-have [|s'x] := boolP (x \in s); last by rewrite Nx0 ?mem_undup ?(count_memPn _).
-rewrite -mem_undup => /perm_to_rem/catCA_perm_subst->; last first.
-  by move=> s1 s2 s3; rewrite /N !map_cat !flatten_cat !count_cat addnCA.
-rewrite /N /= count_cat -/(N x _) Nx0 ?mem_rem_uniq ?undup_uniq ?inE ?eqxx //.
-by rewrite addn0 -{2}(size_nseq (_ s) x) -all_count all_pred1_nseq.
-Qed.
-
 Notation "[ 'seq' E | x <- s , y <- t ]" :=
   (flatten [seq [seq E | y <- t] | x <- s])
   (at level 0, E at level 99, x ident, y ident,
@@ -2820,7 +2849,7 @@ Lemma allpairs_mapr f (g : forall x, T' x -> T x) s t :
   [seq f x y | x <- s, y <- map (g x) (t x)] =
     [seq f x (g x y) | x <- s, y <- t x].
 Proof. by rewrite -(eq_map (fun=> map_comp _ _ _)). Qed.
-
+	
 End AllPairsDep.
 
 Arguments allpairs_dep {S T R} f s t /.
@@ -2949,68 +2978,248 @@ Qed.
 End EqAllPairs.
 
 Arguments allpairsP {S T R f s t z}.
-Arguments perm_eq_nilP {T s}.
-Arguments perm_eq_consP {T x s t}.
+Arguments perm_nilP {T s}.
+Arguments perm_consP {T x s t}.
 
 Section Permutations.
 
 Variable T : eqType.
+Implicit Types (x : T) (s t : seq T) (bs : seq (T * nat)) (acc : seq (seq T)).
+
+Fixpoint incr_tally bs x :=
+  if bs isn't b :: bs then [:: (x, 1)] else
+  if x == b.1 then (x, b.2.+1) :: bs else b :: incr_tally bs x.
+
+Definition tally s := foldl incr_tally [::] s.
+
+Definition wf_tally :=
+  [qualify a bs : seq (T * nat) | uniq (unzip1 bs) && (0 \notin unzip2 bs)].
+
+Definition tally_seq bs := flatten [seq nseq b.2 b.1 | b <- bs].
+Local Notation tseq := tally_seq.
+
+Lemma size_tally_seq bs : size (tally_seq bs) = sumn (unzip2 bs).
+Proof.
+rewrite size_flatten /shape -map_comp; congr sumn.
+by apply/eq_map=> b; apply: size_nseq.
+Qed.
+
+Lemma tally_seqK : {in wf_tally, cancel tally_seq tally}.
+Proof.
+move=> bs /andP[]; elim: bs => [|[x [|n]] bs IHbs] //= /andP[bs'x Ubs] bs'0.
+rewrite inE /tseq /tally /= -[n.+1]addn1 in bs'0 *.
+elim: n 1 => /= [|n IHn] m; last by rewrite eqxx IHn addnS.
+rewrite -{}[in RHS]IHbs {Ubs bs'0}// /tally /tally_seq add0n.
+elim: bs bs'x [::] => [|[y n] bs IHbs] //=; rewrite inE => /norP[y'x bs'x].
+by elim: n => [|n IHn] bs1 /=; [rewrite IHbs | rewrite eq_sym ifN // IHn].
+Qed.
+
+Lemma incr_tallyP x : {homo incr_tally^~ x : bs / bs \in wf_tally}.
+Proof.
+move=> bs /andP[]; rewrite unfold_in.
+elim: bs => [|[y [|n]] bs IHbs] //= /andP[bs'y Ubs]; rewrite inE /= => bs'0.
+rewrite eq_sym; case: ifP => [/eqP<- | y'x] /=; first by rewrite bs'y Ubs.
+rewrite -andbA {}IHbs {Ubs bs'0}// andbT.
+elim: bs bs'y => [|b bs IHbs] /=; rewrite inE ?y'x // => /norP[b'y bs'y].
+by case: ifP => _; rewrite /= inE negb_or ?y'x // b'y IHbs.
+Qed.
+
+Lemma tallyP s : tally s \is a wf_tally.
+Proof.
+rewrite /tally; set bs := [::]; have: bs \in wf_tally by [].
+by elim: s bs => //= x s IHs bs /(incr_tallyP x)/IHs.
+Qed.
+
+Lemma tallyK s : perm_eq (tally_seq (tally s)) s.
+Proof.
+rewrite -[s in perm_eq _ s]cats0 -[nil]/(tseq [::]) /tally.
+elim: s [::] => //= x s IHs bs; rewrite {IHs}(permPl (IHs _)).
+rewrite perm_sym -cat1s perm_catCA {s}perm_cat2l.
+elim: bs => //= b bs IHbs; case: eqP => [-> | _] //=.
+by rewrite -cat1s perm_catCA perm_cat2l.
+Qed.
+
+Lemma tallyEl s : perm_eq (unzip1 (tally s)) (undup s).
+Proof.
+have /andP[Ubs bs'0] := tallyP s; set bs := tally s in Ubs bs'0 *.
+rewrite uniq_perm ?undup_uniq {Ubs}// => x.
+rewrite mem_undup -(perm_mem (tallyK s)) -/bs.
+elim: bs => [|[y [|m]] bs IHbs] //= in bs'0 *.
+by rewrite inE IHbs // mem_cat mem_nseq.
+Qed.
+
+Lemma tallyE s : perm_eq (tally s) [seq (x, count_mem x s) | x <- undup s].
+Proof.
+have /andP[Ubs _] := tallyP s; pose b := [fun s x => (x, count_mem x (tseq s))].
+suffices /permPl->: perm_eq (tally s) (map (b (tally s)) (unzip1 (tally s))).
+  congr perm_eq: (perm_map (b (tally s)) (tallyEl s)).
+  by apply/eq_map=> x; rewrite /= (permP (tallyK s)).
+elim: (tally s) Ubs => [|[x m] bs IH] //= /andP[bs'x /IH-IHbs {IH}].
+rewrite /tseq /= -/(tseq _) count_cat count_nseq /= eqxx mul1n.
+rewrite (count_memPn _) ?addn0 ?perm_cons; last first.
+  apply: contra bs'x; elim: {b IHbs}bs => //= b bs IHbs.
+  by rewrite mem_cat mem_nseq inE andbC; case: (_ == _).
+congr perm_eq: IHbs; apply/eq_in_map=> y bs_y; congr (y, _).
+by rewrite count_cat count_nseq /= (negPf (memPnC bs'x y bs_y)).
+Qed.
 
-Fixpoint permutations (s : seq T) :=
-  if s isn't x :: s1 then [:: nil] else
-  let insert_x t i := take i t ++ x :: drop i t in
-  [seq insert_x t i | t <- permutations s1, i <- iota 0 (index x t + 1)].
+Lemma perm_tally s1 s2 : perm_eq s1 s2 -> perm_eq (tally s1) (tally s2).
+Proof.
+move=> eq_s12; apply: (@perm_trans _ [seq (x, count_mem x s2) | x <- undup s1]).
+  by congr perm_eq: (tallyE s1); apply/eq_map=> x; rewrite (permP eq_s12).
+by rewrite (permPr (tallyE s2)); apply/perm_map/perm_undup/(perm_mem eq_s12).
+Qed.
+
+Lemma perm_tally_seq bs1 bs2 :
+  perm_eq bs1 bs2 -> perm_eq (tally_seq bs1) (tally_seq bs2).
+Proof. by move=> Ebs12; rewrite perm_flatten ?perm_map. Qed.
+Local Notation perm_tseq := perm_tally_seq.
+
+Lemma perm_count_undup s :
+  perm_eq (flatten [seq nseq (count_mem x s) x | x <- undup s]) s.
+Proof.
+by rewrite -(permPr (tallyK s)) (permPr (perm_tseq (tallyE s))) /tseq -map_comp.
+Qed.
+
+Local Fixpoint cons_perms_ perms_rec (s : seq T) bs bs2 acc :=
+  if bs isn't b :: bs1 then acc else
+  if b isn't (x, m.+1) then cons_perms_ perms_rec s bs1 bs2 acc else
+  let acc_xs := perms_rec (x :: s) ((x, m) :: bs1 ++ bs2) acc in
+  cons_perms_ perms_rec s bs1 (b :: bs2) acc_xs.
+
+Local Fixpoint perms_rec n s bs acc :=
+  if n isn't n.+1 then s :: acc else cons_perms_ (perms_rec n) s bs [::] acc.
+Local Notation cons_perms n := (cons_perms_ (perms_rec n) [::]).
+
+Definition permutations s := perms_rec (size s) [::] (tally s) [::].
+
+Let permsP s : exists n bs,
+   [/\ permutations s = perms_rec n [::] bs [::],
+       size (tseq bs) == n, perm_eq (tseq bs) s & uniq (unzip1 bs)].
+Proof.
+have /andP[Ubs _] := tallyP s; exists (size s), (tally s).
+by rewrite (perm_size (tallyK s)) tallyK.
+Qed.
+
+Local Notation bsCA := (permEl (perm_catCA _ [:: _] _)).
+Let cons_permsE : forall n x bs bs1 bs2,
+  let cp := cons_perms n bs bs2 in let perms s := perms_rec n s bs1 [::] in
+  cp (perms [:: x]) = cp [::] ++ [seq rcons t x | t <- perms [::]].
+Proof.
+pose is_acc f := forall acc, f acc = f [::] ++ acc. (* f is accumulating. *)
+have cpE: forall f & forall s bs, is_acc (f s bs), is_acc (cons_perms_ f _ _ _).
+  move=> s bs bs2 f fE acc; elim: bs => [|[x [|m]] bs IHbs] //= in s bs2 acc *.
+  by rewrite fE IHbs catA -IHbs.
+have prE: is_acc (perms_rec _ _ _) by elim=> //= n IHn s bs; apply: cpE.
+pose has_suffix f := forall s : seq T, f s = [seq t ++ s | t <- f [::]].
+suffices prEs n bs: has_suffix (fun s => perms_rec n s bs [::]).
+  move=> n x bs bs1 bs2 /=; rewrite cpE // prEs; congr (_ ++ _).
+  by apply/eq_map=> t; rewrite cats1.
+elim: n bs => //= n IHn bs s; elim: bs [::] => [|[x [|m]] bs IHbs] //= bs1.
+rewrite cpE // IHbs IHn [in RHS]cpE // [in RHS]IHn map_cat -map_comp.
+by congr (_ ++ _); apply: eq_map => t /=; rewrite -catA.
+Qed.
 
 Lemma mem_permutations s t : (t \in permutations s) = perm_eq t s.
 Proof.
-elim: s => [|x s IHs] /= in t *; first by rewrite inE (sameP perm_eq_nilP eqP).
-apply/allpairsPdep/idP=> [[t1 [i [Et1s _ ->]]] | Ets].
-  by rewrite -cat1s perm_catCA /= cat_take_drop perm_cons -IHs.
-pose i := index x t; pose t1 := take i t; pose t2 := drop i.+1 t.
-have sz_t1: size t1 = i by rewrite size_takel ?index_size.
-have t_x: x \in t by rewrite (perm_eq_mem Ets) mem_head.
-have Dt: t = t1 ++ x :: t2.
-  by rewrite -(nth_index x t_x) -drop_nth ?index_mem ?cat_take_drop.
-exists (t1 ++ t2), i; split; last by rewrite take_size_cat ?drop_size_cat.
-  by rewrite IHs -(perm_cons x) -cat1s perm_catCA /= -Dt.
-rewrite mem_iota addn1 ltnS /= /i Dt !index_cat /= eqxx addn0.
-by case: ifP; rewrite ?leq_addr.
+have{s} [n [bs [-> Dn /permPr<- _]]] := permsP s.
+elim: n => [|n IHn] /= in t bs Dn *.
+  by rewrite inE (nilP Dn); apply/eqP/perm_nilP.
+rewrite -[bs in tseq bs]cats0 in Dn *; have x0 : T by case: (tseq _) Dn.
+rewrite -[RHS](@andb_idl (last x0 t \in tseq bs)); last first.
+  case/lastP: t {IHn} => [|t x] Dt; first by rewrite -(perm_size Dt) in Dn.
+  by rewrite -[bs]cats0 -(perm_mem Dt) last_rcons mem_rcons mem_head.
+elim: bs [::] => [|[x [|m]] bs IHbs] //= bs2 in Dn *.
+rewrite cons_permsE -!cat_cons !mem_cat (mem_nseq m.+1) orbC andb_orl.
+rewrite {}IHbs ?(perm_size (perm_tseq bsCA)) //= (permPr (perm_tseq bsCA)).
+congr (_ || _); apply/mapP/andP=> [[t1 Dt1 ->] | [/eqP]].
+  by rewrite last_rcons perm_rcons perm_cons IHn in Dt1 *.
+case/lastP: t => [_ /perm_size//|t y]; rewrite last_rcons perm_rcons => ->.
+by rewrite perm_cons; exists t; rewrite ?IHn.
 Qed.
 
-Lemma permutations_all_uniq s : uniq s -> all uniq (permutations s).
+Lemma permutations_uniq s : uniq (permutations s).
 Proof.
-by move=> Us; apply/allP=> t; rewrite mem_permutations => /perm_eq_uniq->.
+have{s} [n [bs [-> Dn _ Ubs]]] := permsP s.
+elim: n => //= n IHn in bs Dn Ubs *; rewrite -[bs]cats0 /unzip1 in Dn Ubs.
+elim: bs [::] => [|[x [|m]] bs IHbs] //= bs2 in Dn Ubs *.
+  by case/andP: Ubs => _ /IHbs->.
+rewrite /= cons_permsE cat_uniq has_sym andbCA andbC.
+rewrite {}IHbs; first 1 last; first by rewrite (perm_size (perm_tseq bsCA)).
+  by rewrite (perm_uniq (perm_map _ bsCA)).
+rewrite (map_inj_uniq (rcons_injl x)) {}IHn {Dn}//=.
+have: x \notin unzip1 bs by apply: contraL Ubs; rewrite map_cat mem_cat => ->.
+move: {bs2 m Ubs}(perms_rec n _ _ _) (_ :: bs2) => ts.
+elim: bs => [|[y [|m]] bs IHbs] //=; rewrite inE => bs2 /norP[x'y /IHbs//].
+rewrite cons_permsE has_cat negb_or has_map => ->.
+by apply/hasPn=> t _; apply: contra x'y => /mapP[t1 _ /rcons_inj[_ ->]].
+Qed.
+
+Notation perms := permutations.
+Lemma permutationsE s :
+    0 < size s ->
+  perm_eq (perms s) [seq x :: t | x <- undup s, t <- perms (rem x s)].
+Proof.
+move=> nt_s; apply/uniq_perm=> [||t]; first exact: permutations_uniq.
+  apply/allpairs_uniq_dep=> [|x _|]; rewrite ?undup_uniq  ?permutations_uniq //.
+  by case=> [_ _] [x t] _ _ [-> ->].
+rewrite mem_permutations; apply/idP/allpairsPdep=> [Dt | [x [t1 []]]].
+  rewrite -(perm_size Dt) in nt_s; case: t nt_s => // x t _ in Dt *.
+  have s_x: x \in s by rewrite -(perm_mem Dt) mem_head.
+  exists x, t; rewrite mem_undup mem_permutations; split=> //.
+  by rewrite -(perm_cons x) (permPl Dt) perm_to_rem.
+rewrite mem_undup mem_permutations -(perm_cons x) => s_x Dt1 ->.
+by rewrite (permPl Dt1) perm_sym perm_to_rem.
+Qed.
+
+Lemma permutationsErot x s (le_x := fun t => iota 0 (index x t + 1)) :
+  perm_eq (perms (x :: s)) [seq rot i (x :: t) | t <- perms s, i <- le_x t].
+Proof.
+have take'x t i: i <= index x t -> i <= size t /\ x \notin take i t.
+  move=> le_i_x; have le_i_t: i <= size t := leq_trans le_i_x (index_size x t).
+  case: (nthP x) => // -[j lt_j_i /eqP]; rewrite size_takel // in lt_j_i.
+  by rewrite nth_take // [_ == _](before_find x (leq_trans lt_j_i le_i_x)).
+pose xrot t i := rot i (x :: t); pose xrotV t := index x (rev (rot 1 t)).
+have xrotK t: {in le_x t, cancel (xrot t) xrotV}.
+  move=> i; rewrite mem_iota addn1 /xrotV => /take'x[le_i_t ti'x].
+  rewrite -rot_addn ?rev_cat //= rev_cons cat_rcons index_cat mem_rev size_rev.
+  by rewrite ifN // size_takel //= eqxx addn0.
+apply/uniq_perm=> [||t]; first exact: permutations_uniq.
+  apply/allpairs_uniq_dep=> [|t _|]; rewrite ?permutations_uniq ?iota_uniq //.
+  move=> _ _ /allpairsPdep[t [i [_ ? ->]]] /allpairsPdep[u [j [_ ? ->]]] Etu.
+  have Eij: i = j by rewrite -(xrotK t i) // /xrot Etu xrotK.
+  by move: Etu; rewrite Eij => /rot_inj[->].
+rewrite mem_permutations; apply/esym; apply/allpairsPdep/idP=> [[u [i]] | Dt].
+  rewrite mem_permutations => -[Du _ /(canLR (rotK i))]; rewrite /rotr.
+  by set j := (j in rot j _) => Dt; apply/perm_consP; exists j, u.
+pose r := rev (rot 1 t); pose i := index x r; pose u := rev (take i r).
+have r_x: x \in r by rewrite mem_rev mem_rot (perm_mem Dt) mem_head.
+have [v Duv]: {v | rot i (x :: u ++ v) = t}; first exists (rev (drop i.+1 r)).
+  rewrite -rev_cat -rev_rcons -rot1_cons -cat_cons -(nth_index x r_x).
+  by rewrite -drop_nth ?index_mem // rot_rot !rev_rot revK rotK rotrK.
+exists (u ++ v), i; rewrite mem_permutations -(perm_cons x) -(perm_rot i) Duv.
+rewrite mem_iota addn1 ltnS /= index_cat mem_rev size_rev.
+by have /take'x[le_i_t ti'x] := leqnn i; rewrite ifN ?size_takel ?leq_addr.
 Qed.
 
 Lemma size_permutations s : uniq s -> size (permutations s) = (size s)`!.
 Proof.
-elim: s => //= x s IH /andP[s'x /IH-{IH}IHs]; rewrite factS -IHs mulnC.
-rewrite -(size_allpairs mem _ (x :: s)) !size_allpairs_dep.
-congr sumn; apply/eq_in_map => t; rewrite mem_permutations => Est.
-rewrite size_iota -(cats0 t) index_cat (perm_eq_mem Est) addn1 ifN //.
-by rewrite addn0 (perm_eq_size Est).
+move Dn: (size s) => n Us; elim: n s => [[]|n IHn s] //= in Dn Us *.
+rewrite (perm_size (permutationsE _)) ?Dn // undup_id // factS -Dn.
+rewrite -(size_iota 0 n`!) -(size_allpairs (fun=>id)) !size_allpairs_dep.
+by apply/congr1/eq_in_map=> x sx; rewrite size_iota IHn ?size_rem ?Dn ?rem_uniq.
 Qed.
 
-Lemma permutations_uniq s : uniq (permutations s).
+Lemma permutations_all_uniq s : uniq s -> all uniq (permutations s).
 Proof.
-elim: s => //= x s IHs.
-rewrite allpairs_uniq_dep {IHs}// => [t _ |]; first exact: iota_uniq.
-move=> _ _ /allpairsPdep[t [i [_ leix ->]]] /allpairsPdep[u [j [_ lejx ->]]] /=.
-rewrite !mem_iota /= !addn1 !ltnS in leix lejx *; set tx := {-}(_ ++ _).
-gen have Dj, Di: i t @tx leix / ((index x tx = i) * (size (take i t) = i))%type.
-  have Di: size (take i t) = i by apply/size_takel/(leq_trans leix)/index_size.
-  rewrite index_cat /= eqxx addn0 Di ifN //; apply: contraL leix => ti_x.
-  by rewrite -ltnNge -Di -{1}(cat_take_drop i t) index_cat ti_x index_mem.
-move=> eq_tu; have eq_ij: i = j by rewrite -Di eq_tu Dj.
-move/eqP: eq_tu; rewrite eqseq_cat ?Dj // eqseq_cons eqxx /= -eqseq_cat ?Dj //.
-by rewrite !cat_take_drop eq_ij => /eqP->.
+by move=> Us; apply/allP=> t; rewrite mem_permutations => /perm_uniq->.
 Qed.
 
 Lemma perm_permutations s t :
   perm_eq s t -> perm_eq (permutations s) (permutations t).
 Proof.
-move=> Est; apply/uniq_perm_eq; try exact: permutations_uniq.
-by move=> u; rewrite !mem_permutations (perm_eqrP Est).
+move=> Est; apply/uniq_perm; try exact: permutations_uniq.
+by move=> u; rewrite !mem_permutations (permPr Est).
 Qed.
 
 End Permutations.
@@ -3057,14 +3266,40 @@ Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" := (all_iff P0 (P1 :: .. [:: Pn] ..))
   (at level 0, format "[ '<->' '['  P0 ;  '/' P1 ;  '/'  .. ;  '/'  Pn ']' ]")
   : form_scope.
 
+(* Temporary backward compatibility. *)
+Notation perm_eqP := (deprecate perm_eqP permP) (only parsing).
+Notation perm_eqlP := (deprecate perm_eqlP permPl) (only parsing).
+Notation perm_eqrP := (deprecate perm_eqrP permPr) (only parsing).
+Notation perm_eqlE := (deprecate perm_eqlE permEl _ _ _) (only parsing).
+Notation perm_eq_refl := (deprecate perm_eq_refl perm_refl _) (only parsing).
+Notation perm_eq_sym := (deprecate perm_eq_sym perm_sym _) (only parsing).
+Notation "@ 'perm_eq_trans'" := (deprecate perm_eq_trans perm_trans)
+  (at level 10, only parsing).
+Notation perm_eq_trans := (@perm_eq_trans _ _ _ _) (only parsing).
+Notation perm_eq_size := (deprecate perm_eq_size perm_size _ _ _)
+  (only parsing).
+Notation perm_eq_mem := (deprecate perm_eq_mem perm_mem _ _ _)
+  (only parsing).
+Notation perm_eq_uniq := (deprecate perm_eq_uniq perm_uniq _ _ _)
+  (only parsing).
+Notation perm_eq_rev := (deprecate perm_eq_rev perm_rev _)
+  (only parsing).
+Notation perm_eq_flatten := (deprecate perm_eq_flatten perm_flatten _ _ _)
+  (only parsing).
+Notation perm_eq_all := (deprecate perm_eq_all perm_all _ _ _)
+  (only parsing).
+Notation perm_eq_small := (deprecate perm_eq_small perm_small_eq _ _ _)
+  (only parsing).
+Notation perm_eq_nilP := (deprecate perm_eq_nilP perm_nilP) (only parsing).
+Notation perm_eq_consP := (deprecate perm_eq_consP perm_consP) (only parsing).
 Notation leq_size_perm :=
   ((fun T s1 s2 Us1 ss12 les21 =>
    let: (Esz12, Es12) :=
      deprecate leq_size_perm uniq_min_size T s1 s2 Us1 ss12 les21
    in conj Es12 Esz12) _ _ _)
   (only parsing).
-Notation perm_uniq :=
-  ((fun T s1 s2 eq_s12 eq_sz12 =>
-      deprecate perm_uniq eq_uniq T s1 s2 eq_sz12 eq_s12)
-    _ _ _)
+Notation uniq_perm_eq := (deprecate uniq_perm_eq uniq_perm _ _ _)
+  (only parsing).
+Notation perm_eq_iotaP := (deprecate perm_eq_iotaP perm_iotaP) (only parsing).
+Notation perm_undup_count := (deprecate perm_undup_count perm_count_undup _ _)
   (only parsing).
diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v
index 95da9cd..2925496 100644
--- a/mathcomp/ssreflect/ssreflect.v
+++ b/mathcomp/ssreflect/ssreflect.v
@@ -17,6 +17,15 @@ Global Set Bullet Behavior "None".
 (*    --> Usage: Notation old := (deprecate old new) (only parsing).          *)
 (*    --> Caveat: deprecate old new only inherits new's maximal implicits;    *)
 (*        on-demand implicits should be added after : (deprecate old new _).  *)
+(*    --> Caveat 2: if premises or conclusions need to be adjusted, of for    *)
+(*        non-prenex implicits, use the idiom:                                *)
+(*         Notation old := ((fun a1 a2 ... => deprecate old new a1 a2 ...)    *)
+(*                          _ _ ... _) (only printing).                       *)
+(*        where all the implicit a_i's occur first, and correspond to the     *)
+(*        trailing _'s, making sure deprecate old new is fully applied and    *)
+(*        there are _no implicits_ inside the (fun .. => ..) expression. This *)
+(*        is to avoid triggering a bug in SSReflect elaboration that is       *)
+(*        triggered by such evars under binders.                              *)
 (*  Import Deprecation.Silent :: turn off deprecation warning messages.       *)
 (*  Import Deprecation.Reject :: raise an error instead of only warning.      *)
 (******************************************************************************)
-- 
cgit v1.2.3