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

1 files changed, 2 insertions, 2 deletions

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 //.