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
---
 mathcomp/algebra/ssrnum.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'mathcomp/algebra/ssrnum.v')

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.
-- 
cgit v1.2.3