Permutations and other extensions to seq; fintype documentation

- Added `permutations` and some `perm_eq` lemmas suggested by @MrSet
  in #299 (except the link to the coq lib `Permutation` predicate).
  Use insertions to construct permutations. This definition is closer
  to the one proposed by @MrSet, than one using rotations (it adds one
  line to the definition of `permutations` but the proofs become a
  little simpler.)

- Added support for casts on `map` comprehension general terms.

- Added `allpairs_map[lr]` suggested by @pi8027 in #314, but with
  equational proofs; changed `allpairs_comp` to its converse
  `map_allpairs` for consistency.

- Add three `allpairs` extensionality lemmas: for the non-localised,
  dependent localised and non-dependent localised cases; as per
  `eq_in_map`, the latter two are equivalences.

- Documented the `all2` predicate added in #224, and the view
  combinators added in #202.

- Renamed `seq2_ind` to `seq_ind2`, and weakened the induction
  hypothesis, adding a `size` equality assumption.

- Corrected the header to use `<=>` for `bool` predicate
  documentation, and `<->` for `Prop` predicates, following the
  library’s general convention.

- Replaced the `nosimpl` in `rev` with a `Arguments simpl never`
  directive, making it possible to merge the `Rev` section into the
  main `Sequences` section.

- Miscellaneous improvements to proof scripts and file organisation.

- Correct maximal implicits of `constant`.

- Fixes omitted `Prenex Implicit` declaration.

- Other implicits fixes.

- Fix apparent `done` regression It appears `done` now does a weaker
  form of intros, and this broke the `dtuple_onP` proof. Updated the
  proof to eliminate the issue.

(Commit log edited by @CohenCyril during the squash.)

4 files changed, 409 insertions, 266 deletions

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9a0559c..3ea6b8c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -12,7 +12,7 @@ MathComp 1.8.0 is compatible with Coq 8.7, 8.8 and 8.9.
 
 - Companion matrix of a polynomial `companionmx p` and the
   theorems: `companionmxK`, `map_mx_companion` and `companion_map_poly`
-  
+
 - `homoW_in`, `inj_homo_in`, `mono_inj_in`, `anti_mono_in`,
   `total_homo_mono_in`, `homoW`, `inj_homo`, `monoj`, `anti_mono`,
   `total_homo_mono`
@@ -36,6 +36,18 @@ MathComp 1.8.0 is compatible with Coq 8.7, 8.8 and 8.9.
   circular implication `P0 -> P1 -> ... -> Pn -> P0`.
   Related theorems are `all_iffLR` and `all_iffP`
 
+- support for casts in map comprehension notations, e.g.,
+  `[seq E : T | s <- s]`.
+
+- a predicate `all2`, a parallel double `seq` version of `all`.
+
+- some `perm_eq` lemmas: `perm_cat[lr]`, `perm_eq_nilP`,
+  `perm_eq_consP`, `perm_eq_flatten`.
+
+- a function `permutations` that computes a duplicate-free list
+  of all permutations of a given sequence `s` over an `eqType`, along
+  whit its theory.
+
 ### Changed
 
 - Theory of `lersif` and intervals:
@@ -83,20 +95,34 @@ MathComp 1.8.0 is compatible with Coq 8.7, 8.8 and 8.9.
   where `t` may depend on `i`. The notation is now primitive and
   expressed using `flatten` and `map` (see documentation of seq).
   `allpairs` now expands to this notation when fully applied.
-  Added `allpairs_dep` and made it self-expanding as well.
-  Generalized some lemmas in a backward compatible way.
-  Some strictly more general lemmas now have suffix `_dep`.
-
-- Generalised `{ffun A -> R}` to handle dependent functions, and to be
+  + Added `allpairs_dep` and made it self-expanding as well.
+  + Generalized some lemmas in a backward compatible way.
+  + Some strictly more general lemmas now have suffix `_dep`.
+  + Replaced `allpairs_comp` with its converse `map_allpairs`.
+  + Added `allpairs` extensionality lemmas for the following cases:
+    non-localised (`eq_allpairs`), dependent localised
+    (`eq_in_allpairs_dep`) and non-dependent localised
+    (`eq_in_allpairs`); as per `eq_in_map`, the latter two are
+    equivalences.
+
+- Generalized `{ffun A -> R}` to handle dependent functions, and to be
   structurally positive so it can be used in recursive inductive type
   definitions.
-  
+
   Minor backward incompatibilities: `fgraph f` is no longer
   a field accessor, and no longer equal to `val f` as `{ffun A -> R}` is no
   longer a `subType`; some instances of `finfun`, `ffunE`, `ffunK` may not unify
-  with a generic nondependent function type `A -> ?R` due to a bug in
+  with a generic non-dependent function type `A -> ?R` due to a bug in
   Coq version 8.9 or below.
 
+- Renamed double `seq` induction lemma from `seq2_ind` to `seq_ind2`,
+  and weakened its induction hypothesis.
+
+- Replaced the `nosimpl` in `rev` with a `Arguments simpl never`
+  directive.
+
+- Many corrections in implicits declarations.
+
 ### Renamed
 
 Renamings also involve the `_in` suffix counterpart when applicable
@@ -132,6 +158,8 @@ Renamings also involve the `_in` suffix counterpart when applicable
 - Removed duplicated definitions of `tag`, `tagged` and `Tagged`
   from `eqtype.v`. They are already in `ssrfun.v`.
 
+- Miscellaneous improvements to proof scripts and file organisation.
+
 ## [1.7.0] - 2018-04-24
 
 Compatibility with Coq 8.8 and lost compatibility with
@@ -160,7 +188,7 @@ Coq <= 8.5. This release is compatible with Coq 8.6, 8.7 and 8.8.
   implicit, parameter of type `numClosedFieldType`. This could break
   some proofs.
   Every theorem from `ssrnum` that used to be in `algC` changed statement.
-  
+
 - `ltngtP`, `contra_eq`, `contra_neq`, `odd_opp`, `nth_iota`
 
 ### Added
@@ -193,7 +221,7 @@ Major reorganization of the archive.
   that is relevant to her. Note that this introduces a possible
   incompatibility for users of the previous version. A replacement
   scheme is suggested in the installation notes.
-	  
+
 - The archive is now open and based on git. Public mirror at:
   https://github.com/math-comp/math-comp
 
diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v
index fa27e75..73e397d 100644
--- a/mathcomp/solvable/primitive_action.v
+++ b/mathcomp/solvable/primitive_action.v
@@ -165,10 +165,8 @@ Definition ntransitive := [transitive A, on dtuple_on | to * n].
 Lemma dtuple_onP t :
   reflect (injective (tnth t) /\ forall i, tnth t i \in S) (t \in dtuple_on).
 Proof.
-rewrite inE subset_all -map_tnth_enum.
-case: (uniq _) / (injectiveP (tnth t)) => f_inj; last by right; case.
-rewrite -[all _ _]negbK -has_predC has_map has_predC negbK /=.
-by apply: (iffP allP) => [Sf|[]//]; split=> // i; rewrite Sf ?mem_enum.
+rewrite inE subset_all -forallb_tnth -[in uniq t]map_tnth_enum /=.
+by apply: (iffP andP) => -[/injectiveP-f_inj /forallP].
 Qed.
 
 Lemma n_act_dtuple t a :
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 93810ca..c06238c 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -92,9 +92,9 @@ Require Import ssrfun ssrbool eqtype ssrnat seq choice path.
 (*      enum_rank x == the i : 'I_(#|T|) such that enum_val i = x.            *)
 (* enum_rank_in Ax0 x == some i : 'I_(#|A|) such that enum_val i = x if       *)
 (*                     x \in A, given Ax0 : x0 \in A.                         *)
-(*      A \subset B == all x \in A satisfy x \in B.                           *)
-(*      A \proper B == all x \in A satisfy x \in B but not the converse.      *)
-(* [disjoint A & B] == no x \in A satisfies x \in B.                          *)
+(*      A \subset B <=> all x \in A satisfy x \in B.                          *)
+(*      A \proper B <=> all x \in A satisfy x \in B but not the converse.     *)
+(* [disjoint A & B] <=> no x \in A satisfies x \in B.                         *)
 (*        image f A == the sequence of f x for all x : T such that x \in A    *)
 (*                     (where a is an applicative predicate), of length #|P|. *)
 (*                     The codomain of F can be any type, but image f A can   *)
@@ -108,13 +108,13 @@ Require Import ssrfun ssrbool eqtype ssrnat seq choice path.
 (*                     im_y : y \in image f P.                                *)
 (*     invF inj_f y == the x such that f x = y, for inj_j : injective f with  *)
 (*                     f : T -> T.                                            *)
-(*  dinjectiveb A f == the restriction of f : T -> R to A is injective        *)
+(*  dinjectiveb A f <=> the restriction of f : T -> R to A is injective       *)
 (*                     (this is a bolean predicate, R must be an eqType).     *)
-(*     injectiveb f == f : T -> R is injective (boolean predicate).           *)
-(*         pred0b A == no x : T satisfies x \in A.                            *)
-(*    [forall x, P] == P (in which x can appear) is true for all values of x; *)
+(*     injectiveb f <=> f : T -> R is injective (boolean predicate).          *)
+(*         pred0b A <=> no x : T satisfies x \in A.                           *)
+(*    [forall x, P] <=> P (in which x can appear) is true for all values of x *)
 (*                     x must range over a finType.                           *)
-(*    [exists x, P] == P is true for some value of x.                         *)
+(*    [exists x, P] <=> P is true for some value of x.                        *)
 (*      [forall (x | C), P] := [forall x, C ==> P].                           *)
 (*       [forall x in A, P] := [forall (x | x \in A), P].                     *)
 (*      [exists (x | C), P] := [exists x, C && P].                            *)
@@ -123,13 +123,15 @@ Require Import ssrfun ssrbool eqtype ssrnat seq choice path.
 (*   [exists x : T, P], [exists x : T in A, P], etc.                          *)
 (* -> The outer brackets can be omitted when nesting finitary quantifiers,    *)
 (*    e.g., [forall i in I, forall j in J, exists a, f i j == a].             *)
-(*       'forall_pP == view for [forall x, p _], for pP : reflect .. (p _).   *)
-(*       'exists_pP == view for [exists x, p _], for pP : reflect .. (p _).   *)
+(*       'forall_pP <-> view for [forall x, p _], for pP : reflect .. (p _).  *)
+(*       'exists_pP <-> view for [exists x, p _], for pP : reflect .. (p _).  *)
+(*    'forall_in_pP <-> view for [forall x in .., p _], for pP as above.      *)
+(*    'exists_in_pP <-> view for [exists x in .., p _], for pP as above.      *)
 (*     [pick x | P] == Some x, for an x such that P holds, or None if there   *)
 (*                     is no such x.                                          *)
 (*     [pick x : T] == Some x with x : T, provided T is nonempty, else None.  *)
 (*    [pick x in A] == Some x, with x \in A, or None if A is empty.           *)
-(* [pick x in A | P] == Some x, with x \in A s.t. P holds, else None.         *)
+(* [pick x in A | P] == Some x, with x \in A such that P holds, else None.    *)
 (*   [pick x | P & Q] := [pick x | P & Q].                                    *)
 (* [pick x in A | P & Q] := [pick x | P & Q].                                 *)
 (* and (un)typed variants [pick x : T | P], [pick x : T in A], [pick x], etc. *)
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index afc571a..43fd30d 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -60,29 +60,37 @@ Require Import ssrfun ssrbool eqtype ssrnat.
 (*       incr_nth s i == the nat sequence s with item i incremented (s is     *)
 (*                       first padded with 0's to size i+1, if needed).       *)
 (*  ** Predicates:                                                            *)
-(*          nilp s == s is [::].                                              *)
+(*          nilp s <=> s is [::].                                             *)
 (*                 := (size s == 0).                                          *)
 (*         x \in s == x appears in s (this requires an eqType for T).         *)
 (*       index x s == the first index at which x appears in s, or size s if   *)
 (*                    x \notin s.                                             *)
-(*         has p s == the (applicative, boolean) predicate p holds for some   *)
-(*                    item in s.                                              *)
-(*         all p s == p holds for all items in s.                             *)
+(*         has a s <=> a holds for some item in s, where a is an applicative  *)
+(*                     bool predicate.                                        *)
+(*         all a s <=> a holds for all items in s.                            *)
+(*         'has_aP <-> the view reflect (exists2 x, x \in s & A x) (has a s), *)
+(*                     where aP x : reflect (A x) (a x).                      *)
+(*         'all_aP <=> the view for reflect {in s, forall x, A x} (all a s).  *)
+(*      all2 r s t <=> the (bool) relation r holds for all _respective_ items *)
+(*                    in s and t, which must also have the same size, i.e.,   *)
+(*                    for s := [:: x1; ...; x_m] and t := [:: y1; ...; y_n],  *)
+(*                    the condition [&& r x_1 y_1, ..., r x_n y_n & m == n].  *)
 (*        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. *)
-(*      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     *)
+(*      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    *)
 (*                    some m : bitseq (see below).                            *)
-(*   perm_eq s1 s2 == s2 is a permutation of s1, i.e., s1 and s2 have the     *)
+(*   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.                                                *)
+(* --> These left/right transitive versions of perm_eq make it easier to      *)
+(*  chain a sequence of equivalences.                                         *)
 (*  ** Filtering:                                                             *)
 (*           filter p s == the subsequence of s consisting of all the items   *)
 (*                         for which the (boolean) predicate p holds.         *)
@@ -161,11 +169,11 @@ Require Import ssrfun ssrbool eqtype ssrnat.
 (* of two operations. "rev", whose simplifications are not natural, is        *)
 (* protected with nosimpl.                                                    *)
 (*  ** The following are equivalent:                                          *)
-(*  [<-> P0; P1; ..; Pn] == P0, P1, ..., Pn are all equivalent                *)
+(*  [<-> P0; P1; ..; Pn] <-> P0, P1, ..., Pn are all equivalent.              *)
 (*                       := P0 -> P1 -> ... -> Pn -> P0                       *)
-(*  if  T : [<-> P0; P1; ..; Pn]  is such an equivalence, and i, j are in nat *)
-(*  then T i j is a proof of the equivalence Pi <-> Pj between Pi and Pj      *)
-(*  when i (resp j) is out of bound, Pi (resp Pj) defaults to P0              *)
+(*  if T : [<-> P0; P1; ..; Pn]  is such an equivalence, and i, j are in nat  *)
+(*  then T i j is a proof of the equivalence Pi <-> Pj between Pi and Pj;     *)
+(*  when i (resp. j) is out of bounds, Pi (resp. Pj) defaults to P0.          *)
 (******************************************************************************)
 
 Set Implicit Arguments.
@@ -678,7 +686,7 @@ Lemma take_oversize n s : size s <= n -> take n s = s.
 Proof. by elim: s n => [|x s IHs] [|n] //= /IHs->. Qed.
 
 Lemma take_size s : take (size s) s = s.
-Proof. by rewrite take_oversize // leqnn. Qed.
+Proof. exact: take_oversize. Qed.
 
 Lemma take_cons x s :
   take n0 (x :: s) = if n0 is n.+1 then x :: (take n s) else [::].
@@ -703,8 +711,8 @@ by rewrite size_takel // ltnW.
 Qed.
 
 Lemma take_cat s1 s2 :
- take n0 (s1 ++ s2) =
-   if n0 < size s1 then take n0 s1 else s1 ++ take (n0 - size s1) s2.
+  take n0 (s1 ++ s2) =
+    if n0 < size s1 then take n0 s1 else s1 ++ take (n0 - size s1) s2.
 Proof.
 elim: s1 n0 => [|x s1 IHs] [|n] //=.
 by rewrite ltnS subSS -(fun_if (cons x)) -IHs.
@@ -713,12 +721,9 @@ Qed.
 Lemma take_size_cat n s1 s2 : size s1 = n -> take n (s1 ++ s2) = s1.
 Proof. by move <-; elim: s1 => [|x s1 IHs]; rewrite ?take0 //= IHs. Qed.
 
-Lemma takel_cat s1 :
-    n0 <= size s1 ->
-  forall s2, take n0 (s1 ++ s2) = take n0 s1.
+Lemma takel_cat s1 s2 : n0 <= size s1 -> take n0 (s1 ++ s2) = take n0 s1.
 Proof.
-move=> Hn0 s2; rewrite take_cat ltn_neqAle Hn0 andbT.
-by case: (n0 =P size s1) => //= ->; rewrite subnn take0 cats0 take_size.
+by rewrite take_cat; case: ltngtP => // <-; rewrite subnn take0 take_size cats0.
 Qed.
 
 Lemma nth_drop s i : nth (drop n0 s) i = nth s (n0 + i).
@@ -786,46 +791,7 @@ Proof. by rewrite /rot /= take0 drop0 -cats1. Qed.
 
 Fixpoint catrev s1 s2 := if s1 is x :: s1' then catrev s1' (x :: s2) else s2.
 
-End Sequences.
-
-(* rev must be defined outside a Section because Coq's end of section *)
-(* "cooking" removes the nosimpl guard.                               *)
-
-Definition rev T (s : seq T) := nosimpl (catrev s [::]).
-
-Arguments nilP {T s}.
-Arguments all_filterP {T a s}.
-
-Prenex Implicits size head ohead behead last rcons belast.
-Prenex Implicits cat take drop rev rot rotr.
-Prenex Implicits find count nth all has filter.
-
-Notation count_mem x := (count (pred_of_simpl (pred1 x))).
-
-Infix "++" := cat : seq_scope.
-
-Notation "[ 'seq' x <- s | C ]" := (filter (fun x => C%B) s)
- (at level 0, x at level 99,
-  format "[ '[hv' 'seq'  x  <-  s '/ '  |  C ] ']'") : seq_scope.
-Notation "[ 'seq' x <- s | C1 & C2 ]" := [seq x <- s | C1 && C2]
- (at level 0, x at level 99,
-  format "[ '[hv' 'seq'  x  <-  s '/ '  |  C1 '/ '  &  C2 ] ']'") : seq_scope.
-Notation "[ 'seq' x : T <- s | C ]" := (filter (fun x : T => C%B) s)
- (at level 0, x at level 99, only parsing).
-Notation "[ 'seq' x : T <- s | C1 & C2 ]" := [seq x : T <- s | C1 && C2]
- (at level 0, x at level 99, only parsing).
-
-
-(* Double induction/recursion. *)
-Lemma seq2_ind T1 T2 (P : seq T1 -> seq T2 -> Type) :
-    P [::] [::] -> (forall x1 x2 s1 s2, P s1 s2 -> P (x1 :: s1) (x2 :: s2)) ->
-  forall s1 s2, size s1 = size s2 -> P s1 s2.
-Proof. by move=> Pnil Pcons; elim=> [|x s IHs] [] //= x2 s2 [] /IHs/Pcons. Qed.
-
-Section Rev.
-
-Variable T : Type.
-Implicit Types s t : seq T.
+Definition rev s := catrev s [::].
 
 Lemma catrev_catl s t u : catrev (s ++ t) u = catrev t (catrev s u).
 Proof. by elim: s u => /=. Qed.
@@ -848,16 +814,15 @@ Proof. by rewrite -catrev_catr -catrev_catl. Qed.
 Lemma rev_rcons s x : rev (rcons s x) = x :: rev s.
 Proof. by rewrite -cats1 rev_cat. Qed.
 
-Lemma revK : involutive (@rev T).
+Lemma revK : involutive rev.
 Proof. by elim=> //= x s IHs; rewrite rev_cons rev_rcons IHs. Qed.
 
-Lemma nth_rev x0 n s :
-  n < size s -> nth x0 (rev s) n = nth x0 s (size s - n.+1).
+Lemma nth_rev n s : n < size s -> nth (rev s) n = nth s (size s - n.+1).
 Proof.
 elim/last_ind: s => // s x IHs in n *.
 rewrite rev_rcons size_rcons ltnS subSS -cats1 nth_cat /=.
 case: n => [|n] lt_n_s; first by rewrite subn0 ltnn subnn.
-by rewrite -{2}(subnK lt_n_s) -addSnnS leq_addr /= -IHs.
+by rewrite subnSK //= leq_subr IHs.
 Qed.
 
 Lemma filter_rev a s : filter a (rev s) = rev (filter a s).
@@ -872,23 +837,43 @@ Proof. by rewrite !has_count count_rev. Qed.
 Lemma all_rev a s : all a (rev s) = all a s.
 Proof. by rewrite !all_count count_rev size_rev. Qed.
 
-Lemma take_rev s n : take n (rev s) = rev (drop (size s - n) s).
-Proof.
-have /orP[le_s_n | le_n_s] := leq_total (size s) n.
-  by rewrite (eqnP le_s_n) drop0 take_oversize ?size_rev.
-rewrite -[s in LHS](cat_take_drop (size s - n)).
-by rewrite rev_cat take_size_cat // size_rev size_drop subKn.
-Qed.
+End Sequences.
 
-Lemma drop_rev s n : drop n (rev s) = rev (take (size s - n) s).
-Proof.
-rewrite -[s]revK take_rev !revK size_rev -minnE /minn.
-by case: ifP => // /ltnW-le_s_n; rewrite !drop_oversize ?size_rev.
-Qed.
+Prenex Implicits size ncons nseq head ohead behead last rcons belast.
+Arguments seqn {T} n.
+Prenex Implicits cat take drop rot rotr catrev.
+Prenex Implicits find count nth all has filter.
+Arguments rev {T} s : simpl never.
+
+Arguments nilP {T s}.
+Arguments all_filterP {T a s}.
+Arguments rotK n0 {T} s : rename.
+Arguments rot_inj {n0 T} [s1 s2] eq_rot_s12 : rename.
+Arguments revK {T} s : rename.
 
-End Rev.
+Notation count_mem x := (count (pred_of_simpl (pred1 x))).
 
-Arguments revK {T}.
+Infix "++" := cat : seq_scope.
+
+Notation "[ 'seq' x <- s | C ]" := (filter (fun x => C%B) s)
+ (at level 0, x at level 99,
+  format "[ '[hv' 'seq'  x  <-  s '/ '  |  C ] ']'") : seq_scope.
+Notation "[ 'seq' x <- s | C1 & C2 ]" := [seq x <- s | C1 && C2]
+ (at level 0, x at level 99,
+  format "[ '[hv' 'seq'  x  <-  s '/ '  |  C1 '/ '  &  C2 ] ']'") : seq_scope.
+Notation "[ 'seq' x : T <- s | C ]" := (filter (fun x : T => C%B) s)
+ (at level 0, x at level 99, only parsing).
+Notation "[ 'seq' x : T <- s | C1 & C2 ]" := [seq x : T <- s | C1 && C2]
+ (at level 0, x at level 99, only parsing).
+
+(* Double induction/recursion. *)
+Lemma seq_ind2 {S T} (P : seq S -> seq T -> Type) :
+    P [::] [::] ->
+    (forall x y s t, size s = size t -> P s t -> P (x :: s) (y :: t)) ->
+  forall s t, size s = size t -> P s t.
+Proof.
+by move=> Pnil Pcons; elim=> [|x s IHs] [|y t] //= [eq_sz]; apply/Pcons/IHs.
+Qed.
 
 (* Equality and eqType for seq.                                          *)
 
@@ -1010,56 +995,45 @@ Proof. by move=> /negPf xz /negPf yz; case: s => [|t s]//; rewrite xz yz. Qed.
 
 Section Filters.
 
-Variable a : pred T.
+Implicit Type a : pred T.
 
-Lemma hasP s : reflect (exists2 x, x \in s & a x) (has a s).
+Lemma hasP {a s} : reflect (exists2 x, x \in s & a x) (has a s).
 Proof.
 elim: s => [|y s IHs] /=; first by right; case.
-case ay: (a y); first by left; exists y; rewrite ?mem_head.
-apply: (iffP IHs) => [] [x ysx ax]; exists x => //; first exact: mem_behead.
-by case: (predU1P ysx) ax => [->|//]; rewrite ay.
+have [a_y | a'y] := @idP (a y); first by left; exists y; rewrite ?mem_head.
+apply: (iffP IHs) => -[x]; first by exists x; first apply: mem_behead.
+by case/predU1P=> [->|] //; exists x.
 Qed.
 
-Lemma hasPP s aP : (forall x, reflect (aP x) (a x)) ->
-  reflect (exists2 x, x \in s & aP x) (has a s).
-Proof. by move=> vP; apply: (iffP (hasP _)) => -[x?/vP]; exists x. Qed.
-
-Lemma hasPn s : reflect (forall x, x \in s -> ~~ a x) (~~ has a s).
+Lemma allP {a s} : reflect {in s, forall x, a x} (all a s).
 Proof.
-apply: (iffP idP) => not_a_s => [x s_x|].
-  by apply: contra not_a_s => a_x; apply/hasP; exists x.
-by apply/hasP=> [[x s_x]]; apply/negP; apply: not_a_s.
+rewrite -[all _ _]negbK -has_predC.
+apply: (iffP idP) => [s'a' x s_x | a_s]; last by apply/hasP=> /= -[x /a_s->].
+by apply: contraR s'a' => a'x; apply/hasP; exists x.
 Qed.
 
-Lemma allP s : reflect (forall x, x \in s -> a x) (all a s).
-Proof.
-elim: s => [|x s IHs]; first by left.
-rewrite /= andbC; case: IHs => IHs /=.
-  apply: (iffP idP) => [Hx y|]; last by apply; apply: mem_head.
-  by case/predU1P=> [->|Hy]; auto.
-by right=> H; case IHs => y Hy; apply H; apply: mem_behead.
-Qed.
+Lemma hasPn a s : reflect {in s, forall x, ~~ a x} (~~ has a s).
+Proof. by rewrite -all_predC; apply: allP. Qed.
 
-Lemma allPP s aP : (forall x, reflect (aP x) (a x)) ->
-  reflect (forall x, x \in s -> aP x) (all a s).
-Proof. by move=> vP; apply: (iffP (allP _)) => /(_ _ _) /vP. Qed.
+Lemma allPn a s : reflect (exists2 x, x \in s & ~~ a x) (~~ all a s).
+Proof. by rewrite -has_predC; apply: hasP. Qed.
 
-Lemma allPn s : reflect (exists2 x, x \in s & ~~ a x) (~~ all a s).
-Proof.
-elim: s => [|x s IHs]; first by right=> [[x Hx _]].
-rewrite /= andbC negb_and; case: IHs => IHs /=.
-  by left; case: IHs => y Hy Hay; exists y; first apply: mem_behead.
-apply: (iffP idP) => [|[y]]; first by exists x; rewrite ?mem_head.
-by case/predU1P=> [-> // | s_y not_a_y]; case: IHs; exists y.
-Qed.
-
-Lemma mem_filter x s : (x \in filter a s) = a x && (x \in s).
+Lemma mem_filter a x s : (x \in filter a s) = a x && (x \in s).
 Proof.
 rewrite andbC; elim: s => //= y s IHs.
 rewrite (fun_if (fun s' : seq T => x \in s')) !in_cons {}IHs.
 by case: eqP => [->|_]; case (a y); rewrite /= ?andbF.
 Qed.
 
+Variables (a : pred T) (s : seq T) (A : T -> Prop).
+Hypothesis aP : forall x, reflect (A x) (a x).
+
+Lemma hasPP : reflect (exists2 x, x \in s & A x) (has a s).
+Proof. by apply: (iffP hasP) => -[x ? /aP]; exists x. Qed.
+
+Lemma allPP : reflect {in s, forall x, A x} (all a s).
+Proof. by apply: (iffP allP) => a_s x /a_s/aP. Qed.
+
 End Filters.
 
 Notation "'has_ view" := (hasPP _ (fun _ => view))
@@ -1096,18 +1070,14 @@ End EqIn.
 
 Lemma eq_has_r s1 s2 : s1 =i s2 -> has^~ s1 =1 has^~ s2.
 Proof.
-move=> Es12 a; apply/(hasP a s1)/(hasP a s2) => [] [x Hx Hax];
- by exists x; rewrite // ?Es12 // -Es12.
+by move=> Es a; apply/hasP/hasP=> -[x sx ax]; exists x; rewrite ?Es in sx *.
 Qed.
 
 Lemma eq_all_r s1 s2 : s1 =i s2 -> all^~ s1 =1 all^~ s2.
-Proof.
-by move=> Es12 a; apply/(allP a s1)/(allP a s2) => Hs x Hx;
-  apply: Hs; rewrite Es12 in Hx *.
-Qed.
+Proof. by move=> Es a; apply/negb_inj; rewrite -!has_predC (eq_has_r Es). Qed.
 
 Lemma has_sym s1 s2 : has (mem s1) s2 = has (mem s2) s1.
-Proof. by apply/(hasP _ s2)/(hasP _ s1) => [] [x]; exists x. Qed.
+Proof. by apply/hasP/hasP=> -[x]; exists x. Qed.
 
 Lemma has_pred1 x s : has (pred1 x) s = (x \in s).
 Proof. by rewrite -(eq_has (mem_seq1^~ x)) (has_sym [:: x]) /= orbF. Qed.
@@ -1314,7 +1284,7 @@ End EqSeq.
 
 Definition inE := (mem_seq1, in_cons, inE).
 
-Prenex Implicits mem_seq1 uniq undup index.
+Prenex Implicits mem_seq1 constant uniq undup index.
 
 Arguments eqseq {T} !_ !_.
 Arguments eqseqP {T x y}.
@@ -1464,12 +1434,18 @@ apply/perm_eqP/perm_eqP=> 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_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.
 
+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_catAC s1 s2 s3 : perm_eql ((s1 ++ s2) ++ s3) ((s1 ++ s3) ++ s2).
 Proof. by apply/perm_eqlP; rewrite -!catA perm_cat2l perm_catC. Qed.
 
@@ -1578,12 +1554,25 @@ 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.
 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).
+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.
+Qed.
+
 Lemma catCA_perm_ind P :
     (forall s1 s2 s3, P (s1 ++ s2 ++ s3) -> P (s2 ++ s1 ++ s3)) ->
   (forall s1 s2, perm_eq s1 s2 -> P s1 -> P s2).
 Proof.
 move=> PcatCA s1 s2 eq_s12; rewrite -[s1]cats0 -[s2]cats0.
-elim: s2 nil => [| x s2 IHs] s3 in s1 eq_s12 *.
+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.
 rewrite -(cat_take_drop i s1) -catA => /PcatCA.
@@ -1643,14 +1632,31 @@ Qed.
 Lemma rotr_inj : injective (@rotr T n0).
 Proof. exact (can_inj rotrK). Qed.
 
+Lemma take_rev s : take n0 (rev s) = rev (drop (size s - n0) s).
+Proof.
+set m := _ - n0; rewrite -[s in LHS](cat_take_drop m) rev_cat take_cat.
+rewrite size_rev size_drop -minnE minnC ltnNge geq_minl [in take m s]/m /minn.
+by have [_|/eqnP->] := ltnP; rewrite ?subnn take0 cats0.
+Qed.
+
+Lemma drop_rev s : drop n0 (rev s) = rev (take (size s - n0) s).
+Proof.
+set m := _ - n0; rewrite -[s in LHS](cat_take_drop m) rev_cat drop_cat.
+rewrite size_rev size_drop -minnE minnC ltnNge geq_minl /= /m /minn.
+by have [_|/eqnP->] := ltnP; rewrite ?take0 // subnn drop0.
+Qed.
+
 Lemma rev_rotr s : rev (rotr n0 s) = rot n0 (rev s).
 Proof. by rewrite rev_cat -take_rev -drop_rev. Qed.
 
 Lemma rev_rot s : rev (rot n0 s) = rotr n0 (rev s).
-Proof. by rewrite (canRL revK (rev_rotr _)) revK. Qed.
+Proof. by apply: canLR revK _; rewrite rev_rotr revK. Qed.
 
 End RotrLemmas.
 
+Arguments rotrK n0 {T} s : rename.
+Arguments rotr_inj {n0 T} [s1 s2] eq_rotr_s12 : rename.
+
 Section RotCompLemmas.
 
 Variable T : Type.
@@ -1717,11 +1723,11 @@ Lemma mask_cons b m x s : mask (b :: m) (x :: s) = nseq b x ++ mask m s.
 Proof. by case: b. Qed.
 
 Lemma size_mask m s : size m = size s -> size (mask m s) = count id m.
-Proof. by move: m s; apply: seq2_ind => // -[] x m s /= ->. Qed.
+Proof. by move: m s; apply: seq_ind2 => // -[] x m s /= _ ->. Qed.
 
 Lemma mask_cat m1 m2 s1 s2 :
   size m1 = size s1 -> mask (m1 ++ m2) (s1 ++ s2) = mask m1 s1 ++ mask m2 s2.
-Proof. by move: m1 s1; apply: seq2_ind => // -[] m1 x1 s1 /= ->. Qed.
+Proof. by move: m1 s1; apply: seq_ind2 => // -[] m1 x1 s1 /= _ ->. Qed.
 
 Lemma has_mask_cons a b m x s :
   has a (mask (b :: m) (x :: s)) = b && a x || has a (mask m s).
@@ -1742,8 +1748,9 @@ Qed.
 
 Lemma resize_mask m s : {m1 | size m1 = size s & mask m s = mask m1 s}.
 Proof.
-by exists (take (size s) m ++ nseq (size s - size m) false);
-   elim: s m => [|x s IHs] [|b m] //=; rewrite (size_nseq, mask_false, IHs).
+exists (take (size s) m ++ nseq (size s - size m) false).
+  by elim: s m => [|x s IHs] [|b m] //=; rewrite (size_nseq, IHs).
+by elim: s m => [|x s IHs] [|b m] //=; rewrite (mask_false, IHs).
 Qed.
 
 End Mask.
@@ -1787,20 +1794,24 @@ Lemma sub0seq s : subseq [::] s. Proof. by case: s. Qed.
 
 Lemma subseq0 s : subseq s [::] = (s == [::]). Proof. by []. Qed.
 
+Lemma subseq_refl s : subseq s s.
+Proof. by elim: s => //= x s IHs; rewrite eqxx. Qed.
+Hint Resolve subseq_refl : core.
+
 Lemma subseqP s1 s2 :
   reflect (exists2 m, size m = size s2 & s1 = mask m s2) (subseq s1 s2).
 Proof.
 elim: s2 s1 => [|y s2 IHs2] [|x s1].
 - by left; exists [::].
-- by right; do 2!case.
+- by right=> -[m /eqP/nilP->].
 - by left; exists (nseq (size s2).+1 false); rewrite ?size_nseq //= mask_false.
 apply: {IHs2}(iffP (IHs2 _)) => [] [m sz_m def_s1].
   by exists ((x == y) :: m); rewrite /= ?sz_m // -def_s1; case: eqP => // ->.
 case: eqP => [_ | ne_xy]; last first.
-  by case: m def_s1 sz_m => [//|[m []//|m]] -> [<-]; exists m.
+  by case: m def_s1 sz_m => [|[] m] //; [case | move=> -> [<-]; exists m].
 pose i := index true m; have def_m_i: take i m = nseq (size (take i m)) false.
   apply/all_pred1P; apply/(all_nthP true) => j.
-  rewrite size_take ltnNge geq_min negb_or -ltnNge; case/andP=> lt_j_i _.
+  rewrite size_take ltnNge geq_min negb_or -ltnNge => /andP[lt_j_i _].
   rewrite nth_take //= -negb_add addbF -addbT -negb_eqb.
   by rewrite [_ == _](before_find _ lt_j_i).
 have lt_i_m: i < size m.
@@ -1832,10 +1843,6 @@ case/subseqP: (IHs m2 m1) => m sz_m def_s; apply/subseqP.
 by exists (false :: m); rewrite //= sz_m.
 Qed.
 
-Lemma subseq_refl s : subseq s s.
-Proof. by elim: s => //= x s IHs; rewrite eqxx. Qed.
-Hint Resolve subseq_refl : core.
-
 Lemma cat_subseq s1 s2 s3 s4 :
   subseq s1 s3 -> subseq s2 s4 -> subseq (s1 ++ s2) (s3 ++ s4).
 Proof.
@@ -1997,7 +2004,7 @@ Lemma map_rot s : map (rot n0 s) = rot n0 (map s).
 Proof. by rewrite /rot map_cat map_take map_drop. Qed.
 
 Lemma map_rotr s : map (rotr n0 s) = rotr n0 (map s).
-Proof. by apply: canRL (@rotK n0 T2) _; rewrite -map_rot rotrK. Qed.
+Proof. by apply: canRL (rotK n0) _; rewrite -map_rot rotrK. Qed.
 
 Lemma map_rev s : map (rev s) = rev (map s).
 Proof. by elim: s => //= x s IHs; rewrite !rev_cons -!cats1 map_cat IHs. Qed.
@@ -2027,6 +2034,19 @@ Notation "[ 'seq' E | i : T <- s & C ]" :=
   [seq E | i : T <- [seq i : T <- s | C]]
   (at level 0, E at level 99, i ident, only parsing) : seq_scope.
 
+Notation "[ 'seq' E : R | i <- s ]" := (@map _ R (fun i => E) s)
+  (at level 0, E at level 99, i ident, only parsing) : seq_scope.
+
+Notation "[ 'seq' E : R | i <- s & C ]" := [seq E : R | i <- [seq i <- s | C]]
+  (at level 0, E at level 99, i ident, only parsing) : seq_scope.
+
+Notation "[ 'seq' E : R | i : T <- s ]" := (@map T R (fun i : T => E) s)
+  (at level 0, E at level 99, i ident, only parsing) : seq_scope.
+
+Notation "[ 'seq' E : R | i : T <- s & C ]" :=
+  [seq E : R | i : T <- [seq i : T <- s | C]]
+  (at level 0, E at level 99, i ident, only parsing) : seq_scope.
+
 Lemma filter_mask T a (s : seq T) : filter a s = mask (map a s) s.
 Proof. by elim: s => //= x s <-; case: (a x). Qed.
 
@@ -2466,6 +2486,13 @@ Fixpoint zip (s : seq S) (t : seq T) {struct t} :=
 Definition unzip1 := map (@fst S T).
 Definition unzip2 := map (@snd S T).
 
+Fixpoint all2 (r : S -> T -> bool) s t :=
+  match s, t with
+  | [::], [::] => true
+  | x :: s, y :: t => r x y && all2 r s t
+  | _, _ => false
+  end.
+
 Lemma zip_unzip s : zip (unzip1 s) (unzip2 s) = s.
 Proof. by elim: s => [|[x y] s /= ->]. Qed.
 
@@ -2488,7 +2515,7 @@ Qed.
 
 Lemma zip_cat s1 s2 t1 t2 :
   size s1 = size t1 -> zip (s1 ++ s2) (t1 ++ t2) = zip s1 t1 ++ zip s2 t2.
-Proof. by elim: s1 t1 => [|x s IHs] [|y t] //= [/IHs->]. Qed.
+Proof. by move: s1 t1; apply: seq_ind2 => //= x y s1 t1 _ ->. Qed.
 
 Lemma nth_zip x y s t i :
   size s = size t -> nth (x, y) (zip s t) i = (nth x s i, nth y t i).
@@ -2502,21 +2529,23 @@ rewrite size_zip ltnNge geq_min.
 by elim: s t i => [|x s IHs] [|y t] [|i] //=; rewrite ?orbT -?IHs.
 Qed.
 
-Lemma zip_rcons s1 s2 z1 z2 :
-    size s1 = size s2 ->
-  zip (rcons s1 z1) (rcons s2 z2) = rcons (zip s1 s2) (z1, z2).
+Lemma zip_rcons s t x y :
+  size s = size t -> zip (rcons s x) (rcons t y) = rcons (zip s t) (x, y).
 Proof. by move=> eq_sz; rewrite -!cats1 zip_cat //= eq_sz. Qed.
 
-Lemma rev_zip s1 s2 :
-  size s1 = size s2 -> rev (zip s1 s2) = zip (rev s1) (rev s2).
+Lemma rev_zip s t : size s = size t -> rev (zip s t) = zip (rev s) (rev t).
 Proof.
-elim: s1 s2 => [|x s1 IHs] [|y s2] //= [eq_sz].
-by rewrite !rev_cons zip_rcons ?IHs ?size_rev.
+move: s t; apply: seq_ind2 => //= x y s t eq_sz IHs.
+by rewrite !rev_cons IHs zip_rcons ?size_rev.
 Qed.
 
+Lemma all2E r s t :
+  all2 r s t = (size s == size t) && all [pred xy | r xy.1 xy.2] (zip s t).
+Proof. by elim: s t => [|x s IHs] [|y t] //=; rewrite IHs andbCA. Qed.
+
 End Zip.
 
-Prenex Implicits zip unzip1 unzip2.
+Prenex Implicits zip unzip1 unzip2 all2.
 
 Section Flatten.
 
@@ -2724,6 +2753,13 @@ apply: (iffP flattenP) => [[_ /mapP[x sx ->]] | [x sx]] Axy; first by exists x.
 by exists (A x); rewrite ?map_f.
 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.
+by move=> ss1 ss2 ss3; rewrite !flatten_cat !count_cat addnCA.
+Qed.
+
 End EqFlatten.
 
 Arguments flattenP {T A x}.
@@ -2751,32 +2787,52 @@ Notation "[ 'seq' E | x <- s , y <- t ]" :=
 Notation "[ 'seq' E | x : S <- s , y : T <- t ]" :=
   (flatten [seq [seq E | y : T <- t] | x : S  <- s])
   (at level 0, E at level 99, x ident, y ident, only parsing) : seq_scope.
+Notation "[ 'seq' E : R | x : S <- s , y : T <- t ]" :=
+  (flatten [seq [seq E : R | y : T <- t] | x : S  <- s])
+  (at level 0, E at level 99, x ident, y ident, only parsing) : seq_scope.
+Notation "[ 'seq' E : R | x <- s , y <- t ]" :=
+  (flatten [seq [seq E : R | y <- t] | x  <- s])
+  (at level 0, E at level 99, x ident, y ident, only parsing) : seq_scope.
 
 Section AllPairsDep.
 
-Variables (S : Type) (T : S -> Type)  (R : Type) (f : forall x, T x -> R).
-Implicit Types (s : seq S) (t : forall x, seq (T x)).
+Variables (S S' : Type) (T T' : S -> Type) (R : Type).
+Implicit Type f : forall x, T x -> R.
 
-Definition allpairs_dep s t := [seq f y | x <- s, y <- t x].
+Definition allpairs_dep f s t := [seq f x y | x <- s, y <- t x].
 
-Lemma size_allpairs_dep s t :
-  size [seq f y | x <- s, y <- t x] = sumn [seq size (t x) | x <- s].
+Lemma size_allpairs_dep f s t :
+  size [seq f x y | x <- s, y <- t x] = sumn [seq size (t x) | x <- s].
 Proof. by elim: s => //= x s IHs; rewrite size_cat size_map IHs. Qed.
 
-Lemma allpairs_cat s1 s2 t :
-  [seq f y | x <- s1 ++ s2, y <- t x] =
-    [seq f y | x <- s1, y <- t x] ++ [seq f y | x <- s2, y <- t x].
+Lemma eq_allpairs (f1 f2 : forall x, T x -> R) s t :
+    (forall x, f1 x =1 f2 x) ->
+  [seq f1 x y | x <- s, y <- t x] = [seq f2 x y | x <- s, y <- t x].
+Proof. by  move=> eq_f; rewrite (eq_map (fun x => eq_map (eq_f x) (t x))). Qed.
+
+Lemma allpairs_cat f s1 s2 t :
+  [seq f x y | x <- s1 ++ s2, y <- t x] =
+    [seq f x y | x <- s1, y <- t x] ++ [seq f x y | x <- s2, y <- t x].
 Proof. by rewrite map_cat flatten_cat. Qed.
 
-Lemma allpairs_comp R' (g : R -> R') s t :
-  [seq g (f y) | x <- s, y <- t x] =
-    [seq g r | r <- [seq f y | x <- s, y <- t x]].
-Proof. by elim: s => //= x s ->; rewrite map_cat map_comp. Qed.
+Lemma allpairs_mapl f (g : S' -> S) s t :
+  [seq f x y | x <- map g s, y <- t x] = [seq f (g x) y | x <- s, y <- t (g x)].
+Proof. by rewrite -map_comp. Qed.
+
+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 /.
 
+Lemma map_allpairs S T R R' (g : R' -> R) f s t :
+  map g [seq f x y | x : S <- s, y : T x <- t x] =
+    [seq g (f x y) | x <- s, y <- t x].
+Proof. by rewrite map_flatten allpairs_mapl allpairs_mapr. Qed.
+
 Section AllPairsNonDep.
 
 Variables (S T R : Type) (f : S -> T -> R).
@@ -2796,48 +2852,59 @@ Section EqAllPairsDep.
 Variables (S : eqType) (T : S -> eqType).
 Implicit Types (R : eqType) (s : seq S) (t : forall x, seq (T x)).
 
-Lemma allpairsPdep R f s t (z : R) :
+Lemma allpairsPdep R (f : forall x, T x -> R) s t (z : R) :
   reflect (exists x y, [/\ x \in s, y \in t x & z = f x y])
           (z \in [seq f x y | x <- s, y <- t x]).
 Proof.
-apply: (iffP flatten_mapP); first by case=> x ? /mapP[y ? ->]; exists x, y.
-by move=> [x [y [xs yt ->]]]; exists x => //; apply: map_f.
+apply: (iffP flatten_mapP); first by case=> x sx /mapP[y ty ->]; exists x, y.
+by case=> x [y [sx ty ->]]; exists x; last apply: map_f.
 Qed.
 
-Lemma allpairs_f_dep R (f : forall x, T x -> R) s t x y :
+Variable R : eqType.
+Implicit Type f : forall x, T x -> R.
+
+Lemma allpairs_f_dep f s t x y :
   x \in s -> y \in t x -> f x y \in [seq f x y | x <- s, y <- t x].
-Proof. by move=> xs yt; apply/allpairsPdep; exists x, y. Qed.
+Proof. by move=> sx ty; apply/allpairsPdep; exists x, y. Qed.
 
-Lemma mem_allpairs_dep R (f : forall x, T x -> R) s1 t1 s2 t2 :
-    s1 =i s2 -> (forall x, x \in s1 -> t1 x =i t2 x) ->
+Lemma eq_in_allpairs_dep f1 f2 s t :
+    {in s, forall x, {in t x, f1 x =1 f2 x}} <->
+  [seq f1 x y : R | x <- s, y <- t x] = [seq f2 x y | x <- s, y <- t x].
+Proof.
+split=> [eq_f | eq_fst x s_x].
+  by congr flatten; apply/eq_in_map=> x s_x; apply/eq_in_map/eq_f.
+apply/eq_in_map; apply/eq_in_map: x s_x; apply/eq_from_flatten_shape => //.
+by rewrite /shape -!map_comp; apply/eq_map=> x /=; rewrite !size_map.
+Qed.
+
+Lemma mem_allpairs_dep f s1 t1 s2 t2 :
+    s1 =i s2 -> {in s1, forall x, t1 x =i t2 x} ->
   [seq f x y | x <- s1, y <- t1 x] =i [seq f x y | x <- s2, y <- t2 x].
 Proof.
-move=> eq_s eq_t z; apply/allpairsPdep/allpairsPdep=> -[x [y [xs ys ->]]];
-by exists x, y; rewrite ?eq_s ?eq_t// -?eq_s -?eq_t// eq_s.
+move=> eq_s eq_t z; apply/allpairsPdep/allpairsPdep=> -[x [y [sx ty ->]]];
+by exists x, y; rewrite -eq_s in sx *; rewrite eq_t in ty *.
 Qed.
 
-Lemma allpairs_catr R (f : forall x, T x -> R) s t1 t2 :
+Lemma allpairs_catr f s t1 t2 :
   [seq f x y | x <- s, y <- t1 x ++ t2 x] =i
     [seq f x y | x <- s, y <- t1 x] ++ [seq f x y | x <- s, y <- t2 x].
 Proof.
-move=> r; rewrite mem_cat; apply/allpairsPdep/orP=> [[x [y [xs]]]|].
-  by rewrite mem_cat; case/orP; [left|right]; apply/allpairsPdep; exists x, y.
-by case=>/allpairsPdep[x [y [? yt ->]]]; exists x, y; rewrite mem_cat yt ?orbT.
+move=> z; rewrite mem_cat; apply/allpairsPdep/orP=> [[x [y [s_x]]]|].
+  by rewrite mem_cat => /orP[]; [left|right]; apply/allpairsPdep; exists x, y.
+by case=>/allpairsPdep[x [y [sx ty ->]]]; exists x, y; rewrite mem_cat ty ?orbT.
 Qed.
 
-Lemma allpairs_uniq_dep R (f : forall x, T x -> R) s t
-    (g := fun p : {x : S & T x} => f _ (tagged p)) :
-    uniq s -> (forall x, x \in s -> uniq (t x)) ->
-    {in [seq Tagged T y | x <- s, y <- t x] &, injective g} ->
+Lemma allpairs_uniq_dep f s t (st := [seq Tagged T y | x <- s, y <- t x]) :
+  let g (p : {x : S & T x}) : R := f (tag p) (tagged p) in
+    uniq s -> {in s, forall x, uniq (t x)} -> {in st &, injective g} ->
   uniq [seq f x y | x <- s, y <- t x].
 Proof.
-move=> Us Ut gI; have s_s : all (mem s) s by apply/allP.
-rewrite (allpairs_comp (fun=> Tagged T) g) map_inj_in_uniq// {f g gI R}.
-elim: {-1}s s_s Us => //= x s1 IHs /andP[xs s_s1] /andP[xNs1 Us1].
-rewrite cat_uniq {}IHs // andbT map_inj_in_uniq ?Ut //; last first.
-  by move=> y1 y2 _ _ /eqP; rewrite eq_Tagged /= => /eqP.
-apply/hasPn=> _ /allpairsPdep[x1 [y1 [xs1 ys2 ->]]].
-by apply/mapP=> [[y ty [x1_eq _]]]; move: xs1 xNs1; rewrite x1_eq => ->.
+move=> g Us Ut; rewrite -(map_allpairs g (existT T)) => /map_inj_in_uniq->{f g}.
+elim: s Us => //= x s IHs /andP[s'x Us] in st Ut *; rewrite {st}cat_uniq.
+rewrite {}IHs {Us}// ?andbT => [|x1 s_s1]; last exact/Ut/mem_behead.
+have injT: injective (existT T x) by move=> y z /eqP; rewrite eq_Tagged => /eqP.
+rewrite (map_inj_in_uniq (in2W injT)) {injT}Ut ?mem_head // has_sym has_map.
+by apply: contra s'x => /hasP[y _ /allpairsPdep[z [_ [? _ /(congr1 tag)/=->]]]].
 Qed.
 
 End EqAllPairsDep.
@@ -2846,36 +2913,110 @@ Arguments allpairsPdep {S T R f s t z}.
 
 Section EqAllPairs.
 
-Variables S T : eqType.
-Implicit Types (R : eqType) (s : seq S) (t : seq T).
+Variables S T R : eqType.
+Implicit Types (f : S -> T -> R) (s : seq S) (t : seq T).
 
-Lemma allpairsP R (f : S -> T -> R) s t z :
+Lemma allpairsP f s t (z : R) :
   reflect (exists p, [/\ p.1 \in s, p.2 \in t & z = f p.1 p.2])
           (z \in [seq f x y | x <- s, y <- t]).
 Proof.
 by apply: (iffP allpairsPdep) => [[x[y]]|[[x y]]]; [exists (x, y)|exists x, y].
 Qed.
 
-Lemma allpairs_f R (f : S -> T -> R) s t x y :
+Lemma allpairs_f f s t x y :
   x \in s -> y \in t -> f x y \in [seq f x y | x <- s, y <- t].
 Proof. exact: allpairs_f_dep. Qed.
 
-Lemma mem_allpairs R (f : S -> T -> R) s1 t1 s2 t2 : s1 =i s2 -> t1 =i t2 ->
+Lemma eq_in_allpairs f1 f2 s t :
+    {in s & t, f1 =2 f2} <->
+  [seq f1 x y : R | x <- s, y <- t] = [seq f2 x y | x <- s, y <- t].
+Proof.
+split=> [eq_f | /eq_in_allpairs_dep-eq_f x y /eq_f/(_ y)//].
+by apply/eq_in_allpairs_dep=> x /eq_f.
+Qed.
+
+Lemma mem_allpairs f s1 t1 s2 t2 :
+    s1 =i s2 -> t1 =i t2 ->
   [seq f x y | x <- s1, y <- t1] =i [seq f x y | x <- s2, y <- t2].
-Proof. by move=> *; apply: mem_allpairs_dep. Qed.
+Proof. by move=> eq_s eq_t; apply: mem_allpairs_dep. Qed.
 
-Lemma allpairs_uniq R (f : S -> T -> R) s t : uniq s -> uniq t ->
-    {in [seq (x, y) | x <- s, y <- t] &, injective (prod_curry f)} ->
+Lemma allpairs_uniq f s t (st := [seq (x, y) | x <- s, y <- t]) :
+    uniq s -> uniq t -> {in st &, injective (prod_curry f)} ->
   uniq [seq f x y | x <- s, y <- t].
 Proof.
-move=> Us Ut inj_f; apply: allpairs_uniq_dep => //.
-move=> _ _ /allpairsPdep[x [y [xs yt ->]]] /allpairsPdep[u [v [us vt ->]]]/=.
-by move=> /(inj_f (_, _) (_, _)); rewrite !allpairs_f// => /(_ isT isT)[->->].
+move=> Us Ut inj_f; rewrite -(map_allpairs (prod_curry f) (@pair S T)) -/st.
+rewrite map_inj_in_uniq // allpairs_uniq_dep {Us Ut st inj_f}//.
+by apply: in2W => -[x1 y1] [x2 y2] /= [-> ->].
 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}.
+
+Section Permutations.
+
+Variable T : eqType.
+
+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 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.
+Qed.
+
+Lemma permutations_all_uniq s : uniq s -> all uniq (permutations s).
+Proof.
+by move=> Us; apply/allP=> t; rewrite mem_permutations => /perm_eq_uniq->.
+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).
+Qed.
+
+Lemma permutations_uniq s : 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->.
+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).
+Qed.
+
+End Permutations.
 
 Section AllIff.
 (* The Following Are Equivalent *)
@@ -2885,37 +3026,29 @@ Section AllIff.
 Inductive all_iff_and (P Q : Prop) : Prop := AllIffConj of P & Q.
 
 Definition all_iff (P0 : Prop) (Ps : seq Prop) : Prop :=
-  (fix aux (P : Prop) (Qs : seq Prop) : Prop :=
-      if Qs is Q :: Qs then all_iff_and (P -> Q) (aux Q Qs)
-      else P -> P0 : Prop) P0 Ps.
-
-Lemma all_iffLR P0 Ps : all_iff P0 Ps ->
-   forall m n, nth P0 (P0 :: Ps) m -> nth P0 (P0 :: Ps) n.
-Proof.
-have homo_ltn T (f : nat -> T) (r : T -> T -> Prop) : (* #201 *)
-  (forall y x z, r x y -> r y z -> r x z) ->
-  (forall i, r (f i) (f i.+1)) -> {homo f : i j / i < j >-> r i j}.
-  move=> rtrans rfS x y; elim: y x => // y ihy x; rewrite ltnS leq_eqVlt.
-  case/orP=> [/eqP-> // | ltxy]; apply: rtrans (rfS _); exact: ihy.
-move=> Ps_iff; have ltn_imply : {homo nth P0 Ps : m n / m < n >-> (m -> n)}.
-  apply: homo_ltn => [??? xy yz /xy /yz //|i].
-  elim: Ps i P0 Ps_iff => [|P [|/=Q Ps] IHPs] [|i]//= P0 [P0P Ps_iff]//=;
-     do ?by [rewrite nth_nil|case: Ps_iff].
-  by case: Ps_iff => [PQ Ps_iff]; apply: IHPs; split => // /P0P.
-have {ltn_imply}leq_imply : {homo nth P0 Ps : m n / m <= n >-> (m -> n)}.
-  by move=> m n; rewrite leq_eqVlt => /predU1P[->//|/ltn_imply].
-move=> [:P0ton Pnto0] [|m] [|n]//=.
-- abstract: P0ton n.
-  suff P0to0 : P0 -> nth P0 Ps 0 by move=> /P0to0; apply: leq_imply.
-  by case: Ps Ps_iff {leq_imply} => // P Ps [].
-- abstract: Pnto0 m => /(leq_imply m (maxn (size Ps) m)).
-  by rewrite nth_default ?leq_max ?leqnn // orbT ; apply.
-by move=> /Pnto0; apply: P0ton.
-Qed.
-
-Lemma all_iffP P0 Ps : all_iff P0 Ps ->
-   forall m n, nth P0 (P0 :: Ps) m <-> nth P0 (P0 :: Ps) n.
-Proof. by move=> /all_iffLR iffPs m n; split => /iffPs. Qed.
+  let fix loop (P : Prop) (Qs : seq Prop) : Prop :=
+    if Qs is Q :: Qs then all_iff_and (P -> Q) (loop Q Qs) else P -> P0 in
+  loop P0 Ps.
+
+Lemma all_iffLR P0 Ps :
+   all_iff P0 Ps -> forall m n, nth P0 (P0 :: Ps) m -> nth P0 (P0 :: Ps) n.
+Proof.
+move=> iffPs; have PsS n: nth P0 Ps n -> nth P0 Ps n.+1.
+  elim: n P0 Ps iffPs => [|n IHn] P0 [|P [|Q Ps]] //= [iP0P] //; first by case.
+    by rewrite nth_nil.
+  by case=> iPQ iffPs; apply: IHn; split=> // /iP0P.
+have{PsS} lePs: {homo nth P0 Ps : m n / m <= n >-> (m -> n)}.
+  by move=> m n /subnK<-; elim: {n}(n - m) => // n IHn /IHn; apply: PsS.
+move=> m n P_m; have{m P_m} hP0: P0.
+  case: m P_m => //= m /(lePs m _ (leq_maxl m (size Ps))).
+  by rewrite nth_default ?leq_maxr.
+case: n =>// n; apply: lePs 0 n (leq0n n) _.
+by case: Ps iffPs hP0 => // P Ps [].
+Qed.
+
+Lemma all_iffP P0 Ps :
+   all_iff P0 Ps -> forall m n, nth P0 (P0 :: Ps) m <-> nth P0 (P0 :: Ps) n.
+Proof. by move=> /all_iffLR-iffPs m n; split => /iffPs. Qed.
 
 End AllIff.
 Arguments all_iffLR {P0 Ps}.
@@ -2926,21 +3059,3 @@ Coercion all_iffP : all_iff >-> Funclass.
 Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" := (all_iff P0 (P1 :: .. [:: Pn] ..))
   (at level 0, format "[ '<->' '['  P0 ;  '/' P1 ;  '/'  .. ;  '/'  Pn ']' ]")
   : form_scope.
-
-Section All2.
-Context {T U : Type} (p : T -> U -> bool).
-
-Fixpoint all2 s1 s2 :=
-  match s1, s2 with
-  | [::], [::] => true
-  | x1 :: s1, x2 :: s2 => p x1 x2 && all2 s1 s2
-  | _, _ => false
-  end.
-
-Lemma all2E s1 s2 :
-  all2 s1 s2 = (size s1 == size s2) && all [pred xy | p xy.1 xy.2] (zip s1 s2).
-Proof. by elim: s1 s2 => [|x s1 ihs1] [|y s2] //=; rewrite ihs1 andbCA. Qed.
-
-End All2.
-
-Arguments all2 {T U} p !s1 !s2.