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, 1 insertions, 2 deletions

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.