Initial commit

1 files changed, 2552 insertions, 0 deletions

diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
new file mode 100644
index 0000000..8522017
--- /dev/null
+++ b/mathcomp/ssreflect/seq.v
@@ -0,0 +1,2552 @@
+(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+
+(******************************************************************************)
+(* The seq type is the ssreflect type for sequences; it is an alias for the   *)
+(* standard Coq list type. The ssreflect library equips it with many          *)
+(* operations, as well as eqType and predType (and, later, choiceType)        *)
+(* structures. The operations are geared towards reflection: they generally   *)
+(* expect and provide boolean predicates, e.g., the membership predicate      *)
+(* expects an eqType. To avoid any confusion we do not Import the Coq List    *)
+(* module.                                                                    *)
+(*   As there is no true subtyping in Coq, we don't use a type for non-empty  *)
+(* sequences; rather, we pass explicitly the head and tail of the sequence.   *)
+(*   The empty sequence is especially bothersome for subscripting, since it   *)
+(* forces us to pass a default value. This default value can often be hidden  *)
+(* by a notation.                                                             *)
+(*   Here is the list of seq operations:                                      *)
+(*  ** Constructors:                                                          *)
+(*                        seq T == the type of sequences with items of type T *)
+(*                       bitseq == seq bool                                   *)
+(*             [::], nil, Nil T == the empty sequence (of type T)             *)
+(* x :: s, cons x s, Cons T x s == the sequence x followed by s (of type T)   *)
+(*                       [:: x] == the singleton sequence                     *)
+(*           [:: x_0; ...; x_n] == the explicit sequence of the x_i           *)
+(*       [:: x_0, ..., x_n & s] == the sequence of the x_i, followed by s     *)
+(*                    rcons s x == the sequence s, followed by x              *)
+(*  All of the above, except rcons, can be used in patterns. We define a view *)
+(* lastP and an induction principle last_ind that can be used to decompose    *)
+(* or traverse a sequence in a right to left order. The view lemma lastP has  *)
+(* a dependent family type, so the ssreflect tactic case/lastP: p => [|p' x]  *)
+(* will generate two subgoals in which p has been replaced by [::] and by     *)
+(* rcons p' x, respectively.                                                  *)
+(*  ** Factories:                                                             *)
+(*             nseq n x == a sequence of n x's                                *)
+(*          ncons n x s == a sequence of n x's, followed by s                 *)
+(* seqn n x_0 ... x_n-1 == the sequence of the x_i (can be partially applied) *)
+(*             iota m n == the sequence m, m + 1, ..., m + n - 1              *)
+(*            mkseq f n == the sequence f 0, f 1, ..., f (n - 1)              *)
+(*  ** Sequential access:                                                     *)
+(*      head x0 s == the head (zero'th item) of s if s is non-empty, else x0  *)
+(*        ohead s == None if s is empty, else Some x where x is the head of s *)
+(*       behead s == s minus its head, i.e., s' if s = x :: s', else [::]     *)
+(*       last x s == the last element of x :: s (which is non-empty)          *)
+(*     belast x s == x :: s minus its last item                               *)
+(*  ** Dimensions:                                                            *)
+(*         size s == the number of items (length) in s                        *)
+(*       shape ss == the sequence of sizes of the items of the sequence of    *)
+(*                   sequences ss                                             *)
+(*  ** Random access:                                                         *)
+(*         nth x0 s i == the item i of s (numbered from 0), or x0 if s does   *)
+(*                       not have at least i+1 items (i.e., size x <= i)      *)
+(*               s`_i == standard notation for nth x0 s i for a default x0,   *)
+(*                       e.g., 0 for rings.                                   *)
+(*   set_nth x0 s i y == s where item i has been changed to y; if s does not  *)
+(*                       have an item i, it is first padded with copies of x0 *)
+(*                       to size i+1.                                         *)
+(*       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 [::]                                               *)
+(*                 := (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                              *)
+(*        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     *)
+(*                    some m : bitseq (see below).                            *)
+(*   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.                                        *)
+(*  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 rightt of perm_eq  *)
+(*    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          *)
+(* subfilter s : seq sT == when sT has a subType p structure, the sequence    *)
+(*                         of items of type sT corresponding to items of s    *)
+(*                         for which p holds.                                 *)
+(*              rem x s == the subsequence of s, where the first occurrence   *)
+(*                         of x has been removed (compare filter (predC1 x) s *)
+(*                         where ALL occurrences of x are removed).           *)
+(*              undup s == the subsequence of s containing only the first     *)
+(*                         occurrence of each item in s, i.e., s with all     *)
+(*                         duplicates removed.                                *)
+(*             mask m s == the subsequence of s selected by m : bitseq, with  *)
+(*                         item i of s selected by bit i in m (extra items or *)
+(*                         bits are ignored.                                  *)
+(*  ** Surgery:                                                               *)
+(* s1 ++ s2, cat s1 s2 == the concatenation of s1 and s2.                     *)
+(*            take n s == the sequence containing only the first n items of s *)
+(*                        (or all of s if size s <= n).                       *)
+(*            drop n s == s minus its first n items ([::] if size s <= n)     *)
+(*             rot n s == s rotated left n times (or s if size s <= n).       *)
+(*                     := drop n s ++ take n s                                *)
+(*            rotr n s == s rotated right n times (or s if size s <= n).      *)
+(*               rev s == the (linear time) reversal of s.                    *)
+(*        catrev s1 s2 == the reversal of s1 followed by s2 (this is the      *)
+(*                        recursive form of rev).                             *)
+(*  ** Iterators: for s == [:: x_1, ..., x_n], t == [:: y_1, ..., y_m],       *)
+(*        map f s == the sequence [:: f x_1, ..., f x_n].                     *)
+(* allpairs f s t == the sequence of all the f x y, with x and y drawn from   *)
+(*                  s and t, respectively, in row-major order.                *)
+(*               := [:: f x_1 y_1; ...; f x_1 y_m; f x_2 y_1; ...; f x_n y_m] *)
+(*      pmap pf s == the sequence [:: y_i1, ..., y_ik] where i1 < ... < ik,   *)
+(*                   pf x_i = Some y_i, and pf x_j = None iff j is not in     *)
+(*                   {i1, ..., ik}.                                           *)
+(*   foldr f a s == the right fold of s by f (i.e., the natural iterator).    *)
+(*               := f x_1 (f x_2 ... (f x_n a))                               *)
+(*        sumn s == x_1 + (x_2 + ... + (x_n + 0)) (when s : seq nat).         *)
+(*   foldl f a s == the left fold of s by f.                                  *)
+(*               := f (f ... (f a x_1) ... x_n-1) x_n                         *)
+(*   scanl f a s == the sequence of partial accumulators of foldl f a s.      *)
+(*               := [:: f a x_1; ...; foldl f a s]                            *)
+(* pairmap f a s == the sequence of f applied to consecutive items in a :: s. *)
+(*               := [:: f a x_1; f x_1 x_2; ...; f x_n-1 x_n]                 *)
+(*       zip s t == itemwise pairing of s and t (dropping any extra items).   *)
+(*               := [:: (x_1, y_1); ...; (x_mn, y_mn)] with mn = minn n m.    *)
+(*      unzip1 s == [:: (x_1).1; ...; (x_n).1] when s : seq (S * T).          *)
+(*      unzip2 s == [:: (x_1).2; ...; (x_n).2] when s : seq (S * T).          *)
+(*     flatten s == x_1 ++ ... ++ x_n ++ [::] when s : seq (seq T).           *)
+(*   reshape r s == s reshaped into a sequence of sequences whose sizes are   *)
+(*                  given by r (truncating if s is too long or too short).    *)
+(*               := [:: [:: x_1; ...; x_r1];                                  *)
+(*                      [:: x_(r1 + 1); ...; x_(r0 + r1)];                    *)
+(*                      ...;                                                  *)
+(*                      [:: x_(r1 + ... + r(k-1) + 1); ...; x_(r0 + ... rk)]] *)
+(*  ** Notation for manifest comprehensions:                                  *)
+(*         [seq x <- s | C] := filter (fun x => C) s.                         *)
+(*         [seq E | x <- s] := map (fun x => E) s.                            *)
+(* [seq E | x <- s, y <- t] := allpairs (fun x y => E) s t.                   *)
+(*   [seq x <- s | C1 & C2] := [seq x <- s | C1 && C2].                       *)
+(*     [seq E | x <- s & C] := [seq E | x <- [seq x | C]].                    *)
+(*  --> The above allow optional type casts on the eigenvariables, as in      *)
+(*  [seq x : T <- s | C] or [seq E | x : T <- s, y : U <- t]. The cast may be *)
+(*  needed as type inference considers E or C before s.                       *)
+(*   We are quite systematic in providing lemmas to rewrite any composition   *)
+(* of two operations. "rev", whose simplifications are not natural, is        *)
+(* protected with nosimpl.                                                    *)
+(******************************************************************************)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Delimit Scope seq_scope with SEQ.
+Open Scope seq_scope.
+
+(* Inductive seq (T : Type) : Type := Nil | Cons of T & seq T. *)
+Notation seq := list.
+Prenex Implicits cons.
+Notation Cons T := (@cons T) (only parsing).
+Notation Nil T := (@nil T) (only parsing).
+
+Bind Scope seq_scope with list.
+Arguments Scope cons [type_scope _ seq_scope].
+
+(* 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 :: [::])
+  (at level 0, format "[ ::  x1 ]") : seq_scope.
+
+Notation "[ :: x & s ]" := (x :: s) (at level 0, only parsing) : seq_scope.
+
+Notation "[ :: x1 , x2 , .. , xn & s ]" := (x1 :: x2 :: .. (xn :: s) ..)
+  (at level 0, format
+  "'[hv' [ :: '['  x1 , '/'  x2 , '/'  .. , '/'  xn ']' '/ '  &  s ] ']'"
+  ) : seq_scope.
+
+Notation "[ :: x1 ; x2 ; .. ; xn ]" := (x1 :: x2 :: .. [:: xn] ..)
+  (at level 0, format "[ :: '['  x1 ; '/'  x2 ; '/'  .. ; '/'  xn ']' ]"
+  ) : seq_scope.
+
+Section Sequences.
+
+Variable n0 : nat.  (* numerical parameter for take, drop et al *)
+Variable T : Type.  (* must come before the implicit Type     *)
+Variable x0 : T.    (* default for head/nth *)
+
+Implicit Types x y z : T.
+Implicit Types m n : nat.
+Implicit Type s : seq T.
+
+Fixpoint size s := if s is _ :: s' then (size s').+1 else 0.
+
+Lemma size0nil s : size s = 0 -> s = [::]. Proof. by case: s. Qed.
+
+Definition nilp s := size s == 0.
+
+Lemma nilP s : reflect (s = [::]) (nilp s).
+Proof. by case: s => [|x s]; constructor. Qed.
+
+Definition ohead s := if s is x :: _ then Some x else None.
+Definition head s := if s is x :: _ then x else x0.
+
+Definition behead s := if s is _ :: s' then s' else [::].
+
+Lemma size_behead s : size (behead s) = (size s).-1.
+Proof. by case: s. Qed.
+
+(* Factories *)
+
+Definition ncons n x := iter n (cons x).
+Definition nseq n x := ncons n x [::].
+
+Lemma size_ncons n x s : size (ncons n x s) = n + size s.
+Proof. by elim: n => //= n ->. Qed.
+
+Lemma size_nseq n x : size (nseq n x) = n.
+Proof. by rewrite size_ncons addn0. Qed.
+
+(* n-ary, dependently typed constructor. *)
+
+Fixpoint seqn_type n := if n is n'.+1 then T -> seqn_type n' else seq T.
+
+Fixpoint seqn_rec f n : seqn_type n :=
+  if n is n'.+1 return seqn_type n then
+    fun x => seqn_rec (fun s => f (x :: s)) n'
+  else f [::].
+Definition seqn := seqn_rec id.
+
+(* Sequence catenation "cat".                                               *)
+
+Fixpoint cat s1 s2 := if s1 is x :: s1' then x :: s1' ++ s2 else s2
+where "s1 ++ s2" := (cat s1 s2) : seq_scope.
+
+Lemma cat0s s : [::] ++ s = s. Proof. by []. Qed.
+Lemma cat1s x s : [:: x] ++ s = x :: s. Proof. by []. Qed.
+Lemma cat_cons x s1 s2 : (x :: s1) ++ s2 = x :: s1 ++ s2. Proof. by []. Qed.
+
+Lemma cat_nseq n x s : nseq n x ++ s = ncons n x s.
+Proof. by elim: n => //= n ->. Qed.
+
+Lemma cats0 s : s ++ [::] = s.
+Proof. by elim: s => //= x s ->. Qed.
+
+Lemma catA s1 s2 s3 : s1 ++ s2 ++ s3 = (s1 ++ s2) ++ s3.
+Proof. by elim: s1 => //= x s1 ->. Qed.
+
+Lemma size_cat s1 s2 : size (s1 ++ s2) = size s1 + size s2.
+Proof. by elim: s1 => //= x s1 ->. Qed.
+
+(* last, belast, rcons, and last induction. *)
+
+Fixpoint rcons s z := if s is x :: s' then x :: rcons s' z else [:: z].
+
+Lemma rcons_cons x s z : rcons (x :: s) z = x :: rcons s z.
+Proof. by []. Qed.
+
+Lemma cats1 s z : s ++ [:: z] = rcons s z.
+Proof. by elim: s => //= x s ->. Qed.
+
+Fixpoint last x s := if s is x' :: s' then last x' s' else x.
+Fixpoint belast x s := if s is x' :: s' then x :: (belast x' s') else [::].
+
+Lemma lastI x s : x :: s = rcons (belast x s) (last x s).
+Proof. by elim: s x => [|y s IHs] x //=; rewrite IHs. Qed.
+
+Lemma last_cons x y s : last x (y :: s) = last y s.
+Proof. by []. Qed.
+
+Lemma size_rcons s x : size (rcons s x) = (size s).+1.
+Proof. by rewrite -cats1 size_cat addnC. Qed.
+
+Lemma size_belast x s : size (belast x s) = size s.
+Proof. by elim: s x => [|y s IHs] x //=; rewrite IHs. Qed.
+
+Lemma last_cat x s1 s2 : last x (s1 ++ s2) = last (last x s1) s2.
+Proof. by elim: s1 x => [|y s1 IHs] x //=; rewrite IHs. Qed.
+
+Lemma last_rcons x s z : last x (rcons s z) = z.
+Proof. by rewrite -cats1 last_cat. Qed.
+
+Lemma belast_cat x s1 s2 :
+  belast x (s1 ++ s2) = belast x s1 ++ belast (last x s1) s2.
+Proof. by elim: s1 x => [|y s1 IHs] x //=; rewrite IHs. Qed.
+
+Lemma belast_rcons x s z : belast x (rcons s z) = x :: s.
+Proof. by rewrite lastI -!cats1 belast_cat. Qed.
+
+Lemma cat_rcons x s1 s2 : rcons s1 x ++ s2 = s1 ++ x :: s2.
+Proof. by rewrite -cats1 -catA. Qed.
+
+Lemma rcons_cat x s1 s2 : rcons (s1 ++ s2) x = s1 ++ rcons s2 x.
+Proof. by rewrite -!cats1 catA. Qed.
+
+CoInductive last_spec : seq T -> Type :=
+  | LastNil        : last_spec [::]
+  | LastRcons s x  : last_spec (rcons s x).
+
+Lemma lastP s : last_spec s.
+Proof. case: s => [|x s]; [left | rewrite lastI; right]. Qed.
+
+Lemma last_ind P :
+  P [::] -> (forall s x, P s -> P (rcons s x)) -> forall s, P s.
+Proof.
+move=> Hnil Hlast s; rewrite -(cat0s s).
+elim: s [::] Hnil => [|x s2 IHs] s1 Hs1; first by rewrite cats0.
+by rewrite -cat_rcons; auto.
+Qed.
+
+(* Sequence indexing. *)
+
+Fixpoint nth s n {struct n} :=
+  if s is x :: s' then if n is n'.+1 then @nth s' n' else x else x0.
+
+Fixpoint set_nth s n y {struct n} :=
+  if s is x :: s' then if n is n'.+1 then x :: @set_nth s' n' y else y :: s'
+  else ncons n x0 [:: y].
+
+Lemma nth0 s : nth s 0 = head s. Proof. by []. Qed.
+
+Lemma nth_default s n : size s <= n -> nth s n = x0.
+Proof. by elim: s n => [|x s IHs] [|n]; try exact (IHs n). Qed.
+
+Lemma nth_nil n : nth [::] n = x0.
+Proof. by case: n. Qed.
+
+Lemma last_nth x s : last x s = nth (x :: s) (size s).
+Proof. by elim: s x => [|y s IHs] x /=. Qed.
+
+Lemma nth_last s : nth s (size s).-1 = last x0 s.
+Proof. by case: s => //= x s; rewrite last_nth. Qed.
+
+Lemma nth_behead s n : nth (behead s) n = nth s n.+1.
+Proof. by case: s n => [|x s] [|n]. Qed.
+
+Lemma nth_cat s1 s2 n :
+  nth (s1 ++ s2) n = if n < size s1 then nth s1 n else nth s2 (n - size s1).
+Proof. by elim: s1 n => [|x s1 IHs] [|n]; try exact (IHs n). Qed.
+
+Lemma nth_rcons s x n :
+  nth (rcons s x) n =
+    if n < size s then nth s n else if n == size s then x else x0.
+Proof. by elim: s n => [|y s IHs] [|n] //=; rewrite ?nth_nil ?IHs. Qed.
+
+Lemma nth_ncons m x s n :
+  nth (ncons m x s) n = if n < m then x else nth s (n - m).
+Proof. by elim: m n => [|m IHm] [|n] //=; exact: IHm. Qed.
+
+Lemma nth_nseq m x n : nth (nseq m x) n = (if n < m then x else x0).
+Proof. by elim: m n => [|m IHm] [|n] //=; exact: IHm. Qed.
+
+Lemma eq_from_nth s1 s2 :
+    size s1 = size s2 -> (forall i, i < size s1 -> nth s1 i = nth s2 i) ->
+  s1 = s2.
+Proof.
+elim: s1 s2 => [|x1 s1 IHs1] [|x2 s2] //= [eq_sz] eq_s12.
+rewrite [x1](eq_s12 0) // (IHs1 s2) // => i; exact: (eq_s12 i.+1).
+Qed.
+
+Lemma size_set_nth s n y : size (set_nth s n y) = maxn n.+1 (size s).
+Proof.
+elim: s n => [|x s IHs] [|n] //=.
+- by rewrite size_ncons addn1 maxn0.
+- by rewrite maxnE subn1.
+by rewrite IHs -add1n addn_maxr.
+Qed.
+
+Lemma set_nth_nil n y : set_nth [::] n y = ncons n x0 [:: y].
+Proof. by case: n. Qed.
+
+Lemma nth_set_nth s n y : nth (set_nth s n y) =1 [eta nth s with n |-> y].
+Proof.
+elim: s n => [|x s IHs] [|n] [|m] //=; rewrite ?nth_nil ?IHs // nth_ncons eqSS.
+case: ltngtP => // [lt_nm | ->]; last by rewrite subnn.
+by rewrite nth_default // subn_gt0.
+Qed.
+
+Lemma set_set_nth s n1 y1 n2 y2 (s2 := set_nth s n2 y2) :
+  set_nth (set_nth s n1 y1) n2 y2 = if n1 == n2 then s2 else set_nth s2 n1 y1.
+Proof.
+have [-> | ne_n12] := altP eqP.
+  apply: eq_from_nth => [|i _]; first by rewrite !size_set_nth maxnA maxnn.
+  by do 2!rewrite !nth_set_nth /=; case: eqP.
+apply: eq_from_nth => [|i _]; first by rewrite !size_set_nth maxnCA.
+do 2!rewrite !nth_set_nth /=; case: eqP => // ->.
+by rewrite eq_sym -if_neg ne_n12.
+Qed.
+
+(* find, count, has, all. *)
+
+Section SeqFind.
+
+Variable a : pred T.
+
+Fixpoint find s := if s is x :: s' then if a x then 0 else (find s').+1 else 0.
+
+Fixpoint filter s :=
+  if s is x :: s' then if a x then x :: filter s' else filter s' else [::].
+
+Fixpoint count s := if s is x :: s' then a x + count s' else 0.
+
+Fixpoint has s := if s is x :: s' then a x || has s' else false.
+
+Fixpoint all s := if s is x :: s' then a x && all s' else true.
+
+Lemma size_filter s : size (filter s) = count s.
+Proof. by elim: s => //= x s <-; case (a x). Qed.
+
+Lemma has_count s : has s = (0 < count s).
+Proof. by elim: s => //= x s ->; case (a x). Qed.
+
+Lemma count_size s : count s <= size s.
+Proof. by elim: s => //= x s; case: (a x); last exact: leqW. Qed.
+
+Lemma all_count s : all s = (count s == size s).
+Proof.
+elim: s => //= x s; case: (a x) => _ //=.
+by rewrite add0n eqn_leq andbC ltnNge count_size.
+Qed.
+
+Lemma filter_all s : all (filter s).
+Proof. by elim: s => //= x s IHs; case: ifP => //= ->. Qed.
+
+Lemma all_filterP s : reflect (filter s = s) (all s).
+Proof.
+apply: (iffP idP) => [| <-]; last exact: filter_all.
+by elim: s => //= x s IHs /andP[-> Hs]; rewrite IHs.
+Qed.
+
+Lemma filter_id s : filter (filter s) = filter s.
+Proof. by apply/all_filterP; exact: filter_all. Qed.
+
+Lemma has_find s : has s = (find s < size s).
+Proof. by elim: s => //= x s IHs; case (a x); rewrite ?leqnn. Qed.
+
+Lemma find_size s : find s <= size s.
+Proof. by elim: s => //= x s IHs; case (a x). Qed.
+
+Lemma find_cat s1 s2 :
+  find (s1 ++ s2) = if has s1 then find s1 else size s1 + find s2.
+Proof.
+by elim: s1 => //= x s1 IHs; case: (a x) => //; rewrite IHs (fun_if succn).
+Qed.
+
+Lemma has_nil : has [::] = false. Proof. by []. Qed.
+
+Lemma has_seq1 x : has [:: x] = a x.
+Proof. exact: orbF. Qed.
+
+Lemma has_nseq n x : has (nseq n x) = (0 < n) && a x.
+Proof. by elim: n => //= n ->; apply: andKb. Qed.
+
+Lemma has_seqb (b : bool) x : has (nseq b x) = b && a x.
+Proof. by rewrite has_nseq lt0b. Qed.
+
+Lemma all_nil : all [::] = true. Proof. by []. Qed.
+
+Lemma all_seq1 x : all [:: x] = a x.
+Proof. exact: andbT. Qed.
+
+Lemma all_nseq n x : all (nseq n x) = (n == 0) || a x.
+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 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.
+
+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.
+
+Lemma filter_cat s1 s2 : filter (s1 ++ s2) = filter s1 ++ filter s2.
+Proof. by elim: s1 => //= x s1 ->; case (a x). Qed.
+
+Lemma filter_rcons s x :
+  filter (rcons s x) = if a x then rcons (filter s) x else filter s.
+Proof. by rewrite -!cats1 filter_cat /=; case (a x); rewrite /= ?cats0. Qed.
+
+Lemma count_cat s1 s2 : count (s1 ++ s2) = count s1 + count s2.
+Proof. by rewrite -!size_filter filter_cat size_cat. Qed.
+
+Lemma has_cat s1 s2 : has (s1 ++ s2) = has s1 || has s2.
+Proof. by elim: s1 => [|x s1 IHs] //=; rewrite IHs orbA. Qed.
+
+Lemma has_rcons s x : has (rcons s x) = a x || has s.
+Proof. by rewrite -cats1 has_cat has_seq1 orbC. Qed.
+
+Lemma all_cat s1 s2 : all (s1 ++ s2) = all s1 && all s2.
+Proof. by elim: s1 => [|x s1 IHs] //=; rewrite IHs andbA. Qed.
+
+Lemma all_rcons s x : all (rcons s x) = a x && all s.
+Proof. by rewrite -cats1 all_cat all_seq1 andbC. Qed.
+
+End SeqFind.
+
+Lemma eq_find a1 a2 : a1 =1 a2 -> find a1 =1 find a2.
+Proof. by move=> Ea; elim=> //= x s IHs; rewrite Ea IHs. Qed.
+
+Lemma eq_filter a1 a2 : a1 =1 a2 -> filter a1 =1 filter a2.
+Proof. by move=> Ea; elim=> //= x s IHs; rewrite Ea IHs. Qed.
+
+Lemma eq_count a1 a2 : a1 =1 a2 -> count a1 =1 count a2.
+Proof. by move=> Ea s; rewrite -!size_filter (eq_filter Ea). Qed.
+
+Lemma eq_has a1 a2 : a1 =1 a2 -> has a1 =1 has a2.
+Proof. by move=> Ea s; rewrite !has_count (eq_count Ea). Qed.
+
+Lemma eq_all a1 a2 : a1 =1 a2 -> all a1 =1 all a2.
+Proof. by move=> Ea s; rewrite !all_count (eq_count Ea). Qed.
+
+Section SubPred.
+
+Variable (a1 a2 : pred T).
+Hypothesis s12 : subpred a1 a2.
+
+Lemma sub_find s : find a2 s <= find a1 s.
+Proof. by elim: s => //= x s IHs; case: ifP => // /(contraFF (@s12 x))->. Qed.
+
+Lemma sub_has s : has a1 s -> has a2 s.
+Proof. by rewrite !has_find; exact: leq_ltn_trans (sub_find s). Qed.
+
+Lemma sub_count s : count a1 s <= count a2 s.
+Proof.
+by elim: s => //= x s; apply: leq_add; case a1x: (a1 x); rewrite // s12.
+Qed.
+
+Lemma sub_all s : all a1 s -> all a2 s.
+Proof.
+by rewrite !all_count !eqn_leq !count_size => /leq_trans-> //; apply: sub_count.
+Qed.
+
+End SubPred.
+
+Lemma filter_pred0 s : filter pred0 s = [::]. Proof. by elim: s. Qed.
+
+Lemma filter_predT s : filter predT s = s.
+Proof. by elim: s => //= x s ->. Qed.
+
+Lemma filter_predI a1 a2 s : filter (predI a1 a2) s = filter a1 (filter a2 s).
+Proof.
+elim: s => //= x s IHs; rewrite andbC IHs.
+by case: (a2 x) => //=; case (a1 x).
+Qed.
+
+Lemma count_pred0 s : count pred0 s = 0.
+Proof. by rewrite -size_filter filter_pred0. Qed.
+
+Lemma count_predT s : count predT s = size s.
+Proof. by rewrite -size_filter filter_predT. Qed.
+
+Lemma count_predUI a1 a2 s :
+  count (predU a1 a2) s + count (predI a1 a2) s = count a1 s + count a2 s.
+Proof.
+elim: s => //= x s IHs; rewrite /= addnCA -addnA IHs addnA addnC.
+by rewrite -!addnA; do 2 nat_congr; case (a1 x); case (a2 x).
+Qed.
+
+Lemma count_predC a s : count a s + count (predC a) s = size s.
+Proof.
+by elim: s => //= x s IHs; rewrite addnCA -addnA IHs addnA addn_negb.
+Qed.
+
+Lemma count_filter a1 a2 s : count a1 (filter a2 s) = count (predI a1 a2) s.
+Proof. by rewrite -!size_filter filter_predI. Qed.
+
+Lemma has_pred0 s : has pred0 s = false.
+Proof. by rewrite has_count count_pred0. Qed.
+
+Lemma has_predT s : has predT s = (0 < size s).
+Proof. by rewrite has_count count_predT. Qed.
+
+Lemma has_predC a s : has (predC a) s = ~~ all a s.
+Proof. by elim: s => //= x s ->; case (a x). Qed.
+
+Lemma has_predU a1 a2 s : has (predU a1 a2) s = has a1 s || has a2 s.
+Proof. by elim: s => //= x s ->; rewrite -!orbA; do !bool_congr. Qed.
+
+Lemma all_pred0 s : all pred0 s = (size s == 0).
+Proof. by rewrite all_count count_pred0 eq_sym. Qed.
+
+Lemma all_predT s : all predT s.
+Proof. by rewrite all_count count_predT. Qed.
+
+Lemma all_predC a s : all (predC a) s = ~~ has a s.
+Proof. by elim: s => //= x s ->; case (a x). Qed.
+
+Lemma all_predI a1 a2 s : all (predI a1 a2) s = all a1 s && all a2 s.
+Proof.
+apply: (can_inj negbK); rewrite negb_and -!has_predC -has_predU.
+by apply: eq_has => x; rewrite /= negb_and.
+Qed.
+
+(* Surgery: drop, take, rot, rotr.                                        *)
+
+Fixpoint drop n s {struct s} :=
+  match s, n with
+  | _ :: s', n'.+1 => drop n' s'
+  | _, _ => s
+  end.
+
+Lemma drop_behead : drop n0 =1 iter n0 behead.
+Proof. by elim: n0 => [|n IHn] [|x s] //; rewrite iterSr -IHn. Qed.
+
+Lemma drop0 s : drop 0 s = s. Proof. by case: s. Qed.
+
+Lemma drop1 : drop 1 =1 behead. Proof. by case=> [|x [|y s]]. Qed.
+
+Lemma drop_oversize n s : size s <= n -> drop n s = [::].
+Proof. by elim: n s => [|n IHn] [|x s]; try exact (IHn s). Qed.
+
+Lemma drop_size s : drop (size s) s = [::].
+Proof. by rewrite drop_oversize // leqnn. Qed.
+
+Lemma drop_cons x s :
+  drop n0 (x :: s) = if n0 is n.+1 then drop n s else x :: s.
+Proof. by []. Qed.
+
+Lemma size_drop s : size (drop n0 s) = size s - n0.
+Proof. by elim: s n0 => [|x s IHs] [|n]; try exact (IHs n). Qed.
+
+Lemma drop_cat s1 s2 :
+  drop n0 (s1 ++ s2) =
+    if n0 < size s1 then drop n0 s1 ++ s2 else drop (n0 - size s1) s2.
+Proof. by elim: s1 n0 => [|x s1 IHs] [|n]; try exact (IHs n). Qed.
+
+Lemma drop_size_cat n s1 s2 : size s1 = n -> drop n (s1 ++ s2) = s2.
+Proof. by move <-; elim: s1 => //=; rewrite drop0. Qed.
+
+Lemma nconsK n x : cancel (ncons n x) (drop n).
+Proof. by elim: n => //; case. Qed.
+
+Fixpoint take n s {struct s} :=
+  match s, n with
+  | x :: s', n'.+1 => x :: take n' s'
+  | _, _ => [::]
+  end.
+
+Lemma take0 s : take 0 s = [::]. Proof. by case: s. Qed.
+
+Lemma take_oversize n s : size s <= n -> take n s = s.
+Proof. by elim: n s => [|n IHn] [|x s] Hsn; try (congr cons; apply: IHn). Qed.
+
+Lemma take_size s : take (size s) s = s.
+Proof. by rewrite take_oversize // leqnn. Qed.
+
+Lemma take_cons x s :
+  take n0 (x :: s) = if n0 is n.+1 then x :: (take n s) else [::].
+Proof. by []. Qed.
+
+Lemma drop_rcons s : n0 <= size s ->
+  forall x, drop n0 (rcons s x) = rcons (drop n0 s) x.
+Proof. by elim: s n0 => [|y s IHs] [|n]; try exact (IHs n). Qed.
+
+Lemma cat_take_drop s : take n0 s ++ drop n0 s = s.
+Proof. by elim: s n0 => [|x s IHs] [|n]; try exact (congr1 _ (IHs n)). Qed.
+
+Lemma size_takel s : n0 <= size s -> size (take n0 s) = n0.
+Proof.
+by move/subnKC; rewrite -{2}(cat_take_drop s) size_cat size_drop => /addIn.
+Qed.
+
+Lemma size_take s : size (take n0 s) = if n0 < size s then n0 else size s.
+Proof.
+have [le_sn | lt_ns] := leqP (size s) n0; first by rewrite take_oversize.
+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.
+Proof.
+elim: s1 n0 => [|x s1 IHs] [|n] //=.
+by rewrite ltnS subSS -(fun_if (cons x)) -IHs.
+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.
+Proof.
+move=> Hn0 s2; rewrite take_cat ltn_neqAle Hn0 andbT.
+by case: (n0 =P size s1) => //= ->; rewrite subnn take0 cats0 take_size.
+Qed.
+
+Lemma nth_drop s i : nth (drop n0 s) i = nth s (n0 + i).
+Proof.
+have [lt_n0_s | le_s_n0] := ltnP n0 (size s).
+  rewrite -{2}[s]cat_take_drop nth_cat size_take lt_n0_s /= addKn.
+  by rewrite ltnNge leq_addr.
+rewrite !nth_default //; first exact: leq_trans (leq_addr _ _).
+by rewrite size_drop (eqnP le_s_n0).
+Qed.
+
+Lemma nth_take i : i < n0 -> forall s, nth (take n0 s) i = nth s i.
+Proof.
+move=> lt_i_n0 s; case lt_n0_s: (n0 < size s).
+  by rewrite -{2}[s]cat_take_drop nth_cat size_take lt_n0_s /= lt_i_n0.
+by rewrite -{1}[s]cats0 take_cat lt_n0_s /= cats0.
+Qed.
+
+(* drop_nth and take_nth below do NOT use the default n0, because the "n"  *)
+(* can be inferred from the condition, whereas the nth default value x0    *)
+(* will have to be given explicitly (and this will provide "d" as well).   *)
+
+Lemma drop_nth n s : n < size s -> drop n s = nth s n :: drop n.+1 s.
+Proof. by elim: s n => [|x s IHs] [|n] Hn //=; rewrite ?drop0 1?IHs. Qed.
+
+Lemma take_nth n s : n < size s -> take n.+1 s = rcons (take n s) (nth s n).
+Proof. by elim: s n => [|x s IHs] //= [|n] Hn /=; rewrite ?take0 -?IHs. Qed.
+
+(* Rotation *)
+
+Definition rot n s := drop n s ++ take n s.
+
+Lemma rot0 s : rot 0 s = s.
+Proof. by rewrite /rot drop0 take0 cats0. Qed.
+
+Lemma size_rot s : size (rot n0 s) = size s.
+Proof. by rewrite -{2}[s]cat_take_drop /rot !size_cat addnC. Qed.
+
+Lemma rot_oversize n s : size s <= n -> rot n s = s.
+Proof. by move=> le_s_n; rewrite /rot take_oversize ?drop_oversize. Qed.
+
+Lemma rot_size s : rot (size s) s = s.
+Proof. exact: rot_oversize. Qed.
+
+Lemma has_rot s a : has a (rot n0 s) = has a s.
+Proof. by rewrite has_cat orbC -has_cat cat_take_drop. Qed.
+
+Lemma rot_size_cat s1 s2 : rot (size s1) (s1 ++ s2) = s2 ++ s1.
+Proof. by rewrite /rot take_size_cat ?drop_size_cat. Qed.
+
+Definition rotr n s := rot (size s - n) s.
+
+Lemma rotK : cancel (rot n0) (rotr n0).
+Proof.
+move=> s; rewrite /rotr size_rot -size_drop {2}/rot.
+by rewrite rot_size_cat cat_take_drop.
+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.
+
+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 [::]).
+
+Implicit Arguments nilP [T s].
+Implicit Arguments all_filterP [T a s].
+
+Prenex Implicits size nilP head ohead behead last rcons belast.
+Prenex Implicits cat take drop rev rot rotr.
+Prenex Implicits find count nth all has filter all_filterP.
+
+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.
+
+Lemma catrev_catl s t u : catrev (s ++ t) u = catrev t (catrev s u).
+Proof. by elim: s u => /=. Qed.
+
+Lemma catrev_catr s t u : catrev s (t ++ u) = catrev s t ++ u.
+Proof. by elim: s t => //= x s IHs t; rewrite -IHs. Qed.
+
+Lemma catrevE s t : catrev s t = rev s ++ t.
+Proof. by rewrite -catrev_catr. Qed.
+
+Lemma rev_cons x s : rev (x :: s) = rcons (rev s) x.
+Proof. by rewrite -cats1 -catrevE. Qed.
+
+Lemma size_rev s : size (rev s) = size s.
+Proof. by elim: s => // x s IHs; rewrite rev_cons size_rcons IHs. Qed.
+
+Lemma rev_cat s t : rev (s ++ t) = rev t ++ rev s.
+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).
+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).
+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.
+Qed.
+
+Lemma filter_rev a s : filter a (rev s) = rev (filter a s).
+Proof. by elim: s => //= x s IH; rewrite fun_if !rev_cons filter_rcons IH. Qed.
+
+Lemma count_rev a s : count a (rev s) = count a s.
+Proof. by rewrite -!size_filter filter_rev size_rev. Qed.
+
+Lemma has_rev a s : has a (rev s) = has a s.
+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.
+
+End Rev.
+
+Implicit Arguments revK [[T]].
+
+(* Equality and eqType for seq.                                          *)
+
+Section EqSeq.
+
+Variables (n0 : nat) (T : eqType) (x0 : T).
+Notation Local nth := (nth x0).
+Implicit Type s : seq T.
+Implicit Types x y z : T.
+
+Fixpoint eqseq s1 s2 {struct s2} :=
+  match s1, s2 with
+  | [::], [::] => true
+  | x1 :: s1', x2 :: s2' => (x1 == x2) && eqseq s1' s2'
+  | _, _ => false
+  end.
+
+Lemma eqseqP : Equality.axiom eqseq.
+Proof.
+move; elim=> [|x1 s1 IHs] [|x2 s2]; do [by constructor | simpl].
+case: (x1 =P x2) => [<-|neqx]; last by right; case.
+by apply: (iffP (IHs s2)) => [<-|[]].
+Qed.
+
+Canonical seq_eqMixin := EqMixin eqseqP.
+Canonical seq_eqType := Eval hnf in EqType (seq T) seq_eqMixin.
+
+Lemma eqseqE : eqseq = eq_op. Proof. by []. Qed.
+
+Lemma eqseq_cons x1 x2 s1 s2 :
+  (x1 :: s1 == x2 :: s2) = (x1 == x2) && (s1 == s2).
+Proof. by []. Qed.
+
+Lemma eqseq_cat s1 s2 s3 s4 :
+  size s1 = size s2 -> (s1 ++ s3 == s2 ++ s4) = (s1 == s2) && (s3 == s4).
+Proof.
+elim: s1 s2 => [|x1 s1 IHs] [|x2 s2] //= [sz12].
+by rewrite !eqseq_cons -andbA IHs.
+Qed.
+
+Lemma eqseq_rcons s1 s2 x1 x2 :
+  (rcons s1 x1 == rcons s2 x2) = (s1 == s2) && (x1 == x2).
+Proof. by rewrite -(can_eq revK) !rev_rcons eqseq_cons andbC (can_eq revK). Qed.
+
+Lemma size_eq0 s : (size s == 0) = (s == [::]).
+Proof. exact: (sameP nilP eqP). Qed.
+
+Lemma has_filter a s : has a s = (filter a s != [::]).
+Proof. by rewrite -size_eq0 size_filter has_count lt0n. Qed.
+
+(* mem_seq and index. *)
+(* mem_seq defines a predType for seq. *)
+
+Fixpoint mem_seq (s : seq T) :=
+  if s is y :: s' then xpredU1 y (mem_seq s') else xpred0.
+
+Definition eqseq_class := seq T.
+Identity Coercion seq_of_eqseq : eqseq_class >-> seq.
+
+Coercion pred_of_eq_seq (s : eqseq_class) : pred_class := [eta mem_seq s].
+
+Canonical seq_predType := @mkPredType T (seq T) pred_of_eq_seq.
+(* The line below makes mem_seq a canonical instance of topred. *)
+Canonical mem_seq_predType := mkPredType mem_seq.
+
+Lemma in_cons y s x : (x \in y :: s) = (x == y) || (x \in s).
+Proof. by []. Qed.
+
+Lemma in_nil x : (x \in [::]) = false.
+Proof. by []. Qed.
+
+Lemma mem_seq1 x y : (x \in [:: y]) = (x == y).
+Proof. by rewrite in_cons orbF. Qed.
+
+ (* to be repeated after the Section discharge. *)
+Let inE := (mem_seq1, in_cons, inE).
+
+Lemma mem_seq2 x y1 y2 : (x \in [:: y1; y2]) = xpred2 y1 y2 x.
+Proof. by rewrite !inE. Qed.
+
+Lemma mem_seq3  x y1 y2 y3 : (x \in [:: y1; y2; y3]) = xpred3 y1 y2 y3 x.
+Proof. by rewrite !inE. Qed.
+
+Lemma mem_seq4  x y1 y2 y3 y4 :
+  (x \in [:: y1; y2; y3; y4]) = xpred4 y1 y2 y3 y4 x.
+Proof. by rewrite !inE. Qed.
+
+Lemma mem_cat x s1 s2 : (x \in s1 ++ s2) = (x \in s1) || (x \in s2).
+Proof. by elim: s1 => //= y s1 IHs; rewrite !inE /= -orbA -IHs. Qed.
+
+Lemma mem_rcons s y : rcons s y =i y :: s.
+Proof. by move=> x; rewrite -cats1 /= mem_cat mem_seq1 orbC in_cons. Qed.
+
+Lemma mem_head x s : x \in x :: s.
+Proof. exact: predU1l. Qed.
+
+Lemma mem_last x s : last x s \in x :: s.
+Proof. by rewrite lastI mem_rcons mem_head. Qed.
+
+Lemma mem_behead s : {subset behead s <= s}.
+Proof. by case: s => // y s x; exact: predU1r. Qed.
+
+Lemma mem_belast s y : {subset belast y s <= y :: s}.
+Proof. by move=> x ys'x; rewrite lastI mem_rcons mem_behead. Qed.
+
+Lemma mem_nth s n : n < size s -> nth s n \in s.
+Proof.
+by elim: s n => [|x s IHs] // [_|n sz_s]; rewrite ?mem_head // mem_behead ?IHs.
+Qed.
+
+Lemma mem_take s x : x \in take n0 s -> x \in s.
+Proof. by move=> s0x; rewrite -(cat_take_drop n0 s) mem_cat /= s0x. Qed.
+
+Lemma mem_drop s x : x \in drop n0 s -> x \in s.
+Proof. by move=> s0'x; rewrite -(cat_take_drop n0 s) mem_cat /= s0'x orbT. Qed.
+
+Section Filters.
+
+Variable a : pred T.
+
+Lemma hasP 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.
+Qed.
+
+Lemma hasPn s : reflect (forall x, x \in s -> ~~ a x) (~~ has 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; exact: not_a_s.
+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; exact: mem_head.
+  by case/predU1P=> [->|Hy]; auto.
+by right=> H; case IHs => y Hy; apply H; exact: mem_behead.
+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 exact: 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).
+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.
+
+End Filters.
+
+Section EqIn.
+
+Variables a1 a2 : pred T.
+
+Lemma eq_in_filter s : {in s, a1 =1 a2} -> filter a1 s = filter a2 s.
+Proof.
+elim: s => //= x s IHs eq_a.
+rewrite eq_a ?mem_head ?IHs // => y s_y; apply: eq_a; exact: mem_behead.
+Qed.
+
+Lemma eq_in_find s : {in s, a1 =1 a2} -> find a1 s = find a2 s.
+Proof.
+elim: s => //= x s IHs eq_a12; rewrite eq_a12 ?mem_head // IHs // => y s'y.
+by rewrite eq_a12 // mem_behead.
+Qed.
+
+Lemma eq_in_count s : {in s, a1 =1 a2} -> count a1 s = count a2 s.
+Proof. by move/eq_in_filter=> eq_a12; rewrite -!size_filter eq_a12. Qed.
+
+Lemma eq_in_all s : {in s, a1 =1 a2} -> all a1 s = all a2 s.
+Proof. by move=> eq_a12; rewrite !all_count eq_in_count. Qed.
+
+Lemma eq_in_has s : {in s, a1 =1 a2} -> has a1 s = has a2 s.
+Proof. by move/eq_in_filter=> eq_a12; rewrite !has_filter eq_a12. Qed.
+
+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.
+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.
+
+Lemma has_sym s1 s2 : has (mem s1) s2 = has (mem s2) s1.
+Proof. by apply/(hasP _ s2)/(hasP _ s1) => [] [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.
+
+Lemma mem_rev s : rev s =i s.
+Proof. by move=> a; rewrite -!has_pred1 has_rev. Qed.
+
+(* Constant sequences, i.e., the image of nseq. *)
+
+Definition constant s := if s is x :: s' then all (pred1 x) s' else true.
+
+Lemma all_pred1P x s : reflect (s = nseq (size s) x) (all (pred1 x) s).
+Proof.
+elim: s => [|y s IHs] /=; first by left.
+case: eqP => [->{y} | ne_xy]; last by right=> [] [? _]; case ne_xy.
+by apply: (iffP IHs) => [<- //| []].
+Qed.
+
+Lemma all_pred1_constant x s : all (pred1 x) s -> constant s.
+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 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.
+
+Lemma constant_nseq n x : constant (nseq n x).
+Proof. exact: all_pred1_constant (all_pred1_nseq x n). Qed.
+
+(* Uses x0 *)
+Lemma constantP s : reflect (exists x, s = nseq (size s) x) (constant s).
+Proof.
+apply: (iffP idP) => [| [x ->]]; last exact: constant_nseq.
+case: s => [|x s] /=; first by exists x0.
+by move/all_pred1P=> def_s; exists x; rewrite -def_s.
+Qed.
+
+(* Duplicate-freenes. *)
+
+Fixpoint uniq s := if s is x :: s' then (x \notin s') && uniq s' else true.
+
+Lemma cons_uniq x s : uniq (x :: s) = (x \notin s) && uniq s.
+Proof. by []. Qed.
+
+Lemma cat_uniq s1 s2 :
+  uniq (s1 ++ s2) = [&& uniq s1, ~~ has (mem s1) s2 & uniq s2].
+Proof.
+elim: s1 => [|x s1 IHs]; first by rewrite /= has_pred0.
+by rewrite has_sym /= mem_cat !negb_or has_sym IHs -!andbA; do !bool_congr.
+Qed.
+
+Lemma uniq_catC s1 s2 : uniq (s1 ++ s2) = uniq (s2 ++ s1).
+Proof. by rewrite !cat_uniq has_sym andbCA andbA andbC. Qed.
+
+Lemma uniq_catCA s1 s2 s3 : uniq (s1 ++ s2 ++ s3) = uniq (s2 ++ s1 ++ s3).
+Proof.
+by rewrite !catA -!(uniq_catC s3) !(cat_uniq s3) uniq_catC !has_cat orbC.
+Qed.
+
+Lemma rcons_uniq s x : uniq (rcons s x) = (x \notin s) && uniq s.
+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.
+Qed.
+
+Lemma rot_uniq s : uniq (rot n0 s) = uniq s.
+Proof. by rewrite /rot uniq_catC cat_take_drop. Qed.
+
+Lemma rev_uniq s : uniq (rev s) = uniq s.
+Proof.
+elim: s => // x s IHs.
+by rewrite rev_cons -cats1 cat_uniq /= andbT andbC mem_rev orbF IHs.
+Qed.
+
+Lemma count_memPn x s : reflect (count_mem x s = 0) (x \notin s).
+Proof. by rewrite -has_pred1 has_count -eqn0Ngt; apply: eqP. Qed.
+
+Lemma count_uniq_mem s x : uniq s -> count_mem x s = (x \in s).
+Proof.
+elim: s => //= y s IHs /andP[/negbTE s'y /IHs-> {IHs}].
+by rewrite in_cons eq_sym; case: eqP => // ->; rewrite s'y.
+Qed.
+
+Lemma filter_pred1_uniq s x : uniq s -> x \in s -> filter (pred1 x) s = [:: x].
+Proof.
+move=> uniq_s s_x; rewrite (all_pred1P _ _ (filter_all _ _)).
+by rewrite size_filter count_uniq_mem ?s_x.
+Qed.
+
+(* Removing duplicates *)
+
+Fixpoint undup s :=
+  if s is x :: s' then if x \in s' then undup s' else x :: undup s' else [::].
+
+Lemma size_undup s : size (undup s) <= size s.
+Proof. by elim: s => //= x s IHs; case: (x \in s) => //=; exact: 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 => // ->.
+Qed.
+
+Lemma undup_uniq s : uniq (undup s).
+Proof.
+by elim: s => //= x s IHs; case s_x: (x \in s); rewrite //= mem_undup s_x.
+Qed.
+
+Lemma undup_id s : uniq s -> undup s = s.
+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.
+Qed.
+
+Lemma filter_undup p s : filter p (undup s) = undup (filter p s).
+Proof.
+elim: s => //= x s IHs; rewrite (fun_if undup) fun_if /= mem_filter /=.
+by rewrite (fun_if (filter p)) /= IHs; case: ifP => -> //=; exact: if_same.
+Qed.
+
+Lemma undup_nil s : undup s = [::] -> s = [::].
+Proof. by case: s => //= x s; rewrite -mem_undup; case: ifP; case: undup. Qed.
+
+(* Lookup *)
+
+Definition index x := find (pred1 x).
+
+Lemma index_size x s : index x s <= size s.
+Proof. by rewrite /index find_size. Qed.
+
+Lemma index_mem x s : (index x s < size s) = (x \in s).
+Proof. by rewrite -has_pred1 has_find. Qed.
+
+Lemma nth_index x s : x \in s -> nth s (index x s) = x.
+Proof. by rewrite -has_pred1 => /(nth_find x0)/eqP. Qed.
+
+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.
+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.
+Qed.
+
+Lemma index_head x s : index x (x :: s) = 0.
+Proof. by rewrite /= eqxx. Qed.
+
+Lemma index_last x s : uniq (x :: s) -> index (last x s) (x :: s) = size s.
+Proof.
+rewrite lastI rcons_uniq -cats1 index_cat size_belast.
+by case: ifP => //=; rewrite eqxx addn0.
+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.
+
+Lemma mem_rot s : rot n0 s =i s.
+Proof. by move=> x; rewrite -{2}(cat_take_drop n0 s) !mem_cat /= orbC. Qed.
+
+Lemma eqseq_rot s1 s2 : (rot n0 s1 == rot n0 s2) = (s1 == s2).
+Proof. by apply: inj_eq; exact: rot_inj. Qed.
+
+CoInductive rot_to_spec s x := RotToSpec i s' of rot i s = x :: s'.
+
+Lemma rot_to s x : x \in s -> rot_to_spec s x.
+Proof.
+move=> s_x; pose i := index x s; exists i (drop i.+1 s ++ take i s).
+rewrite -cat_cons {}/i; congr cat; elim: s s_x => //= y s IHs.
+by rewrite eq_sym in_cons; case: eqP => // -> _; rewrite drop0.
+Qed.
+
+End EqSeq.
+
+Definition inE := (mem_seq1, in_cons, inE).
+
+Prenex Implicits mem_seq1 uniq undup index.
+
+Implicit Arguments eqseqP [T x y].
+Implicit Arguments hasP [T a s].
+Implicit Arguments hasPn [T a s].
+Implicit Arguments allP [T a s].
+Implicit Arguments allPn [T a s].
+Implicit Arguments nseqP [T n x y].
+Implicit Arguments count_memPn [T x s].
+Prenex Implicits eqseqP hasP hasPn allP allPn nseqP count_memPn.
+
+Section NthTheory.
+
+Lemma nthP (T : eqType) (s : seq T) x x0 :
+  reflect (exists2 i, i < size s & nth x0 s i = x) (x \in s).
+Proof.
+apply: (iffP idP) => [|[n Hn <-]]; last by apply mem_nth.
+by exists (index x s); [rewrite index_mem | apply nth_index].
+Qed.
+
+Variable T : Type.
+
+Lemma has_nthP (a : pred T) s x0 :
+  reflect (exists2 i, i < size s & a (nth x0 s i)) (has a s).
+Proof.
+elim: s => [|x s IHs] /=; first by right; case.
+case nax: (a x); first by left; exists 0.
+by apply: (iffP IHs) => [[i]|[[|i]]]; [exists i.+1 | rewrite nax | exists i].
+Qed.
+
+Lemma all_nthP (a : pred T) s x0 :
+  reflect (forall i, i < size s -> a (nth x0 s i)) (all a s).
+Proof.
+rewrite -(eq_all (fun x => negbK (a x))) all_predC.
+case: (has_nthP _ _ x0) => [na_s | a_s]; [right=> a_s | left=> i lti].
+  by case: na_s => i lti; rewrite a_s.
+by apply/idPn=> na_si; case: a_s; exists i.
+Qed.
+
+End NthTheory.
+
+Lemma set_nth_default T s (y0 x0 : T) n : n < size s -> nth x0 s n = nth y0 s n.
+Proof. by elim: s n => [|y s' IHs] [|n] /=; auto. Qed.
+
+Lemma headI T s (x : T) : rcons s x = head x s :: behead (rcons s x).
+Proof. by case: s. Qed.
+
+Implicit Arguments nthP [T s x].
+Implicit Arguments has_nthP [T a s].
+Implicit Arguments all_nthP [T a s].
+Prenex Implicits nthP has_nthP all_nthP.
+
+Definition bitseq := seq bool.
+Canonical bitseq_eqType := Eval hnf in [eqType of bitseq].
+Canonical bitseq_predType := Eval hnf in [predType of bitseq].
+
+(* Incrementing the ith nat in a seq nat, padding with 0's if needed. This  *)
+(* allows us to use nat seqs as bags of nats.                               *)
+
+Fixpoint incr_nth v i {struct i} :=
+  if v is n :: v' then if i is i'.+1 then n :: incr_nth v' i' else n.+1 :: v'
+  else ncons i 0 [:: 1].
+
+Lemma nth_incr_nth v i j : nth 0 (incr_nth v i) j = (i == j) + nth 0 v j.
+Proof.
+elim: v i j => [|n v IHv] [|i] [|j] //=; rewrite ?eqSS ?addn0 //; try by case j.
+elim: i j => [|i IHv] [|j] //=; rewrite ?eqSS //; by case j.
+Qed.
+
+Lemma size_incr_nth v i :
+  size (incr_nth v i) = if i < size v then size v else i.+1.
+Proof.
+elim: v i => [|n v IHv] [|i] //=; first by rewrite size_ncons /= addn1.
+rewrite IHv; exact: fun_if.
+Qed.
+
+(* Equality up to permutation *)
+
+Section PermSeq.
+
+Variable T : eqType.
+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).
+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.
+have [/eqP|] := posnP (count a (s1 ++ s2)).
+  by rewrite count_cat addn_eq0; do 2!case: eqP => // ->.
+rewrite -has_count => /hasP[x s12x a_x]; pose a' := predD1 a x.
+have cnt_a' s: count a s = count_mem x s + count a' s.
+  rewrite -count_predUI -[LHS]addn0 -(count_pred0 s).
+  by congr (_ + _); apply: eq_count => y /=; case: eqP => // ->.
+rewrite !cnt_a' (eqnP (eq_cnt1 _ s12x)) (IHn a') // -ltnS.
+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.
+
+Lemma perm_eq_sym : symmetric perm_eq.
+Proof. by move=> s1 s2; apply/perm_eqP/perm_eqP=> ? ?. Qed.
+
+Lemma perm_eq_trans : transitive perm_eq.
+Proof. by move=> s2 s1 s3 /perm_eqP-eq12 /perm_eqP/(ftrans eq12)/perm_eqP. 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 perm_eqlP 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.
+Qed.
+
+Lemma perm_eqrP 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.
+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.
+
+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;
+  by move/(_ a)/eqP: eq23; rewrite !count_cat eqn_add2l.
+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; exact: perm_cat2l. 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.
+
+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.
+
+Lemma perm_rcons x s : perm_eql (rcons s x) (x :: s).
+Proof. by move=> /= s2; rewrite -cats1 perm_catC. Qed.
+
+Lemma perm_rot n s : perm_eql (rot n s) s.
+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_filterC a s : perm_eql (filter a s ++ filter (predC a) s) s.
+Proof.
+apply/perm_eqlP; 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_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_eq_small s1 s2 : size s2 <= 1 -> perm_eq s1 s2 -> s1 = s2.
+Proof.
+move=> s2_le1 eqs12; move/perm_eq_size: eqs12 s2_le1 (perm_eq_mem eqs12).
+by case: s2 s1 => [|x []] // [|y []] // _ _ /(_ x); rewrite !inE eqxx => /eqP->.
+Qed.
+
+Lemma uniq_leq_size s1 s2 : uniq s1 -> {subset s1 <= s2} -> size s1 <= size s2.
+Proof.
+elim: s1 s2 => //= x s1 IHs s2 /andP[not_s1x Us1] /allP/=/andP[s2x /allP ss12].
+have [i s3 def_s2] := rot_to s2x; rewrite -(size_rot i s2) def_s2.
+apply: IHs => // y s1y; have:= ss12 y s1y.
+by rewrite -(mem_rot i) def_s2 inE (negPf (memPn _ y s1y)).
+Qed.
+
+Lemma leq_size_uniq s1 s2 :
+  uniq s1 -> {subset s1 <= s2} -> size s2 <= size s1 -> uniq s2.
+Proof.
+elim: s1 s2 => [[] | x s1 IHs s2] // Us1x; have /andP[not_s1x Us1] := Us1x.
+case/allP/andP=> /rot_to[i s3 def_s2] /allP ss12 le_s21.
+rewrite -(rot_uniq i) -(size_rot i) def_s2 /= in le_s21 *.
+have ss13 y (s1y : y \in s1): y \in s3.
+  by have:= ss12 y s1y; rewrite -(mem_rot i) def_s2 inE (negPf (memPn _ y s1y)).
+rewrite IHs // andbT; apply: contraL _ le_s21 => s3x; rewrite -leqNgt.
+by apply/(uniq_leq_size Us1x)/allP; rewrite /= s3x; exact/allP.
+Qed.
+
+Lemma uniq_size_uniq s1 s2 :
+  uniq s1 -> s1 =i s2 -> uniq s2 = (size s2 == size s1).
+Proof.
+move=> Us1 eqs12; apply/idP/idP=> [Us2 | /eqP eq_sz12].
+  by rewrite eqn_leq !uniq_leq_size // => y; rewrite eqs12.
+by apply: (leq_size_uniq Us1) => [y|]; rewrite (eqs12, eq_sz12).
+Qed.
+
+Lemma leq_size_perm s1 s2 :
+    uniq s1 -> {subset s1 <= s2} -> size s2 <= size s1 ->
+  s1 =i s2 /\ size s1 = size s2.
+Proof.
+move=> Us1 ss12 le_s21; have Us2: uniq s2 := leq_size_uniq Us1 ss12 le_s21.
+suffices: s1 =i s2 by split; last by apply/eqP; rewrite -uniq_size_uniq.
+move=> x; apply/idP/idP=> [/ss12// | s2x]; apply: contraLR le_s21 => not_s1x.
+rewrite -ltnNge (@uniq_leq_size (x :: s1)) /= ?not_s1x //.
+by apply/allP; rewrite /= s2x; apply/allP.
+Qed.
+
+Lemma perm_uniq s1 s2 : s1 =i s2 -> size s1 = size s2 -> uniq s1 = uniq s2.
+Proof.
+move=> Es12 Esz12.
+by apply/idP/idP=> Us; rewrite (uniq_size_uniq Us) ?Esz12 ?eqxx.
+Qed.
+
+Lemma perm_eq_uniq s1 s2 : perm_eq s1 s2 -> uniq s1 = uniq s2.
+Proof.
+by move=> eq_s12; apply: perm_uniq; [apply: perm_eq_mem | apply: perm_eq_size].
+Qed.
+
+Lemma uniq_perm_eq 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.
+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.
+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 *.
+  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.
+rewrite catA -/(rot i s1) def_s1 /= -cat1s => /PcatCA/IHs/PcatCA; apply.
+by rewrite -(perm_cons x) -def_s1 perm_rot.
+Qed.
+
+Lemma catCA_perm_subst R F :
+    (forall s1 s2 s3, F (s1 ++ s2 ++ s3) = F (s2 ++ s1 ++ s3) :> R) ->
+  (forall s1 s2, perm_eq s1 s2 -> F s1 = F s2).
+Proof.
+move=> FcatCA s1 s2 /catCA_perm_ind => ind_s12.
+by apply: (ind_s12 (eq _ \o F)) => //= *; rewrite FcatCA.
+Qed.
+
+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).
+
+Implicit Arguments perm_eqP [T s1 s2].
+Implicit Arguments perm_eqlP [T s1 s2].
+Implicit Arguments perm_eqrP [T s1 s2].
+Prenex Implicits perm_eq perm_eqP perm_eqlP perm_eqrP.
+Hint Resolve perm_eq_refl.
+
+Section RotrLemmas.
+
+Variables (n0 : nat) (T : Type) (T' : eqType).
+Implicit Type s : seq T.
+
+Lemma size_rotr s : size (rotr n0 s) = size s.
+Proof. by rewrite size_rot. Qed.
+
+Lemma mem_rotr (s : seq T') : rotr n0 s =i s.
+Proof. by move=> x; rewrite mem_rot. Qed.
+
+Lemma rotr_size_cat s1 s2 : rotr (size s2) (s1 ++ s2) = s2 ++ s1.
+Proof. by rewrite /rotr size_cat addnK rot_size_cat. Qed.
+
+Lemma rotr1_rcons x s : rotr 1 (rcons s x) = x :: s.
+Proof. by rewrite -rot1_cons rotK. Qed.
+
+Lemma has_rotr a s : has a (rotr n0 s) = has a s.
+Proof. by rewrite has_rot. Qed.
+
+Lemma rotr_uniq (s : seq T') : uniq (rotr n0 s) = uniq s.
+Proof. by rewrite rot_uniq. Qed.
+
+Lemma rotrK : cancel (@rotr T n0) (rot n0).
+Proof.
+move=> s; have [lt_n0s | ge_n0s] := ltnP n0 (size s).
+  by rewrite -{1}(subKn (ltnW lt_n0s)) -{1}[size s]size_rotr; exact: rotK.
+by rewrite -{2}(rot_oversize ge_n0s) /rotr (eqnP ge_n0s) rot0.
+Qed.
+
+Lemma rotr_inj : injective (@rotr T n0).
+Proof. exact (can_inj rotrK). Qed.
+
+Lemma rev_rot s : rev (rot n0 s) = rotr n0 (rev s).
+Proof.
+rewrite /rotr size_rev -{3}(cat_take_drop n0 s) {1}/rot !rev_cat.
+by rewrite -size_drop -size_rev rot_size_cat.
+Qed.
+
+Lemma rev_rotr s : rev (rotr n0 s) = rot n0 (rev s).
+Proof.
+apply: canRL rotrK _; rewrite {1}/rotr size_rev size_rotr /rotr {2}/rot rev_cat.
+set m := size s - n0; rewrite -{1}(@size_takel m _ _ (leq_subr _ _)).
+by rewrite -size_rev rot_size_cat -rev_cat cat_take_drop.
+Qed.
+
+End RotrLemmas.
+
+Section RotCompLemmas.
+
+Variable T : Type.
+Implicit Type s : seq T.
+
+Lemma rot_addn m n s : m + n <= size s -> rot (m + n) s = rot m (rot n s).
+Proof.
+move=> sz_s; rewrite {1}/rot -[take _ s](cat_take_drop n).
+rewrite 5!(catA, =^~ rot_size_cat) !cat_take_drop.
+by rewrite size_drop !size_takel ?leq_addl ?addnK.
+Qed.
+
+Lemma rotS n s : n < size s -> rot n.+1 s = rot 1 (rot n s).
+Proof. exact: (@rot_addn 1). Qed.
+
+Lemma rot_add_mod m n s : n <= size s -> m <= size s ->
+  rot m (rot n s) = rot (if m + n <= size s then m + n else m + n - size s) s.
+Proof.
+move=> Hn Hm; case: leqP => [/rot_addn // | /ltnW Hmn]; symmetry.
+by rewrite -{2}(rotK n s) /rotr -rot_addn size_rot addnBA ?subnK ?addnK.
+Qed.
+
+Lemma rot_rot m n s : rot m (rot n s) = rot n (rot m s).
+Proof.
+case: (ltnP (size s) m) => Hm.
+  by rewrite !(@rot_oversize T m) ?size_rot 1?ltnW.
+case: (ltnP (size s) n) => Hn.
+  by rewrite !(@rot_oversize T n) ?size_rot 1?ltnW.
+by rewrite !rot_add_mod 1?addnC.
+Qed.
+
+Lemma rot_rotr m n s : rot m (rotr n s) = rotr n (rot m s).
+Proof. by rewrite {2}/rotr size_rot rot_rot. Qed.
+
+Lemma rotr_rotr m n s : rotr m (rotr n s) = rotr n (rotr m s).
+Proof. by rewrite /rotr !size_rot rot_rot. Qed.
+
+End RotCompLemmas.
+
+Section Mask.
+
+Variables (n0 : nat) (T : Type).
+Implicit Types (m : bitseq) (s : seq T).
+
+Fixpoint mask m s {struct m} :=
+  match m, s with
+  | b :: m', x :: s' => if b then x :: mask m' s' else mask m' s'
+  | _, _ => [::]
+  end.
+
+Lemma mask_false s n : mask (nseq n false) s = [::].
+Proof. by elim: s n => [|x s IHs] [|n] /=. Qed.
+
+Lemma mask_true s n : size s <= n -> mask (nseq n true) s = s.
+Proof. by elim: s n => [|x s IHs] [|n] //= Hn; congr (_ :: _); apply: IHs. Qed.
+
+Lemma mask0 m : mask m [::] = [::].
+Proof. by case: m. Qed.
+
+Lemma mask1 b x : mask [:: b] [:: x] = nseq b x.
+Proof. by case: b. Qed.
+
+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.
+
+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.
+
+Lemma has_mask_cons a b m x s :
+  has a (mask (b :: m) (x :: s)) = b && a x || has a (mask m s).
+Proof. by case: b. Qed.
+
+Lemma has_mask a m s : has a (mask m s) -> has a s.
+Proof.
+elim: m s => [|b m IHm] [|x s] //; rewrite has_mask_cons /= andbC.
+by case: (a x) => //= /IHm.
+Qed.
+
+Lemma mask_rot m s : size m = size s ->
+   mask (rot n0 m) (rot n0 s) = rot (count id (take n0 m)) (mask m s).
+Proof.
+move=> Ems; rewrite mask_cat ?size_drop ?Ems // -rot_size_cat.
+by rewrite size_mask -?mask_cat ?size_take ?Ems // !cat_take_drop.
+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).
+Qed.
+
+End Mask.
+
+Section EqMask.
+
+Variables (n0 : nat) (T : eqType).
+Implicit Types (s : seq T) (m : bitseq).
+
+Lemma mem_mask_cons x b m y s :
+  (x \in mask (b :: m) (y :: s)) = b && (x == y) || (x \in mask m s).
+Proof. by case: b. Qed.
+
+Lemma mem_mask x m s : x \in mask m s -> x \in s.
+Proof. by rewrite -!has_pred1 => /has_mask. Qed.
+
+Lemma mask_uniq s : uniq s -> forall m, uniq (mask m s).
+Proof.
+elim: s => [|x s IHs] Uxs [|b m] //=.
+case: b Uxs => //= /andP[s'x Us]; rewrite {}IHs // andbT.
+by apply: contra s'x; exact: mem_mask.
+Qed.
+
+Lemma mem_mask_rot m s :
+  size m = size s -> mask (rot n0 m) (rot n0 s) =i mask m s.
+Proof. by move=> Ems x; rewrite mask_rot // mem_rot. Qed.
+
+End EqMask.
+
+Section Subseq.
+
+Variable T : eqType.
+Implicit Type s : seq T.
+
+Fixpoint subseq s1 s2 :=
+  if s2 is y :: s2' then
+    if s1 is x :: s1' then subseq (if x == y then s1' else s1) s2' else true
+  else s1 == [::].
+
+Lemma sub0seq s : subseq [::] s. Proof. by case: s. Qed.
+
+Lemma subseq0 s : subseq s [::] = (s == [::]). Proof. by []. Qed.
+
+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 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.
+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 nth_take //= -negb_add addbF -addbT -negb_eqb.
+  by rewrite [_ == _](before_find _ lt_j_i).
+have lt_i_m: i < size m.
+  rewrite ltnNge; apply/negP=> le_m_i; rewrite take_oversize // in def_m_i.
+  by rewrite def_m_i mask_false in def_s1.
+rewrite size_take lt_i_m in def_m_i.
+exists (take i m ++ drop i.+1 m).
+  rewrite size_cat size_take size_drop lt_i_m.
+  by rewrite sz_m in lt_i_m *; rewrite subnKC.
+rewrite {s1 def_s1}[s1](congr1 behead def_s1).
+rewrite -[s2](cat_take_drop i) -{1}[m](cat_take_drop i) {}def_m_i -cat_cons.
+have sz_i_s2: size (take i s2) = i by apply: size_takel; rewrite sz_m in lt_i_m.
+rewrite lastI cat_rcons !mask_cat ?size_nseq ?size_belast ?mask_false //=.
+by rewrite (drop_nth true) // nth_index -?index_mem.
+Qed.
+
+Lemma mask_subseq m s : subseq (mask m s) s.
+Proof. by apply/subseqP; have [m1] := resize_mask m s; exists m1. Qed.
+
+Lemma subseq_trans : transitive subseq.
+Proof.
+move=> _ _ s /subseqP[m2 _ ->] /subseqP[m1 _ ->].
+elim: s => [|x s IHs] in m2 m1 *; first by rewrite !mask0.
+case: m1 => [|[] m1]; first by rewrite mask0.
+  case: m2 => [|[] m2] //; first by rewrite /= eqxx IHs.
+  case/subseqP: (IHs m2 m1) => m sz_m def_s; apply/subseqP.
+  by exists (false :: m); rewrite //= sz_m.
+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.
+
+Lemma cat_subseq s1 s2 s3 s4 :
+  subseq s1 s3 -> subseq s2 s4 -> subseq (s1 ++ s2) (s3 ++ s4).
+Proof.
+case/subseqP=> m1 sz_m1 ->; case/subseqP=> m2 sz_m2 ->; apply/subseqP.
+by exists (m1 ++ m2); rewrite ?size_cat ?mask_cat ?sz_m1 ?sz_m2.
+Qed.
+
+Lemma prefix_subseq s1 s2 : subseq s1 (s1 ++ s2).
+Proof. by rewrite -{1}[s1]cats0 cat_subseq ?sub0seq. Qed.
+
+Lemma suffix_subseq s1 s2 : subseq s2 (s1 ++ s2).
+Proof. by rewrite -{1}[s2]cat0s cat_subseq ?sub0seq. Qed.
+
+Lemma mem_subseq s1 s2 : subseq s1 s2 -> {subset s1 <= s2}.
+Proof. by case/subseqP=> m _ -> x; exact: mem_mask. Qed.
+
+Lemma sub1seq x s : subseq [:: x] s = (x \in s).
+Proof.
+by elim: s => //= y s; rewrite inE; case: (x == y); rewrite ?sub0seq.
+Qed.
+
+Lemma size_subseq s1 s2 : subseq s1 s2 -> size s1 <= size s2.
+Proof. by case/subseqP=> m sz_m ->; rewrite size_mask -sz_m ?count_size. Qed.
+
+Lemma size_subseq_leqif s1 s2 :
+  subseq s1 s2 -> size s1 <= size s2 ?= iff (s1 == s2).
+Proof.
+move=> sub12; split; first exact: size_subseq.
+apply/idP/eqP=> [|-> //]; case/subseqP: sub12 => m sz_m ->{s1}.
+rewrite size_mask -sz_m // -all_count -(eq_all eqb_id).
+by move/(@all_pred1P _ true)->; rewrite sz_m mask_true.
+Qed.
+
+Lemma subseq_cons s x : subseq s (x :: s).
+Proof. by exact: (@cat_subseq [::] s [:: x]). Qed.
+
+Lemma subseq_rcons s x : subseq s (rcons s x).
+Proof. by rewrite -{1}[s]cats0 -cats1 cat_subseq. Qed.
+
+Lemma subseq_uniq s1 s2 : subseq s1 s2 -> uniq s2 -> uniq s1.
+Proof. by case/subseqP=> m _ -> Us2; exact: mask_uniq. Qed.
+
+End Subseq.
+
+Prenex Implicits subseq.
+Implicit Arguments subseqP [T s1 s2].
+
+Hint Resolve subseq_refl.
+
+Section Rem.
+
+Variables (T : eqType) (x : T).
+
+Fixpoint rem s := if s is y :: t then (if y == x then t else y :: rem t) else s.
+
+Lemma rem_id s : x \notin s -> rem s = s.
+Proof.
+by elim: s => //= y s IHs /norP[neq_yx /IHs->]; rewrite eq_sym (negbTE neq_yx).
+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.
+case: eqP => [-> // | _ /IHs].
+by rewrite (perm_catCA [:: x] [:: y]) perm_cons perm_eq_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.
+
+Lemma rem_subseq s : subseq (rem s) s.
+Proof.
+elim: s => //= y s IHs; rewrite eq_sym.
+by case: ifP => _; [exact: subseq_cons | rewrite eqxx].
+Qed.
+
+Lemma rem_uniq s : uniq s -> uniq (rem s).
+Proof. by apply: subseq_uniq; exact: rem_subseq. Qed.
+
+Lemma mem_rem s : {subset rem s <= s}.
+Proof. exact: mem_subseq (rem_subseq s). Qed.
+
+Lemma rem_filter s : uniq s -> rem s = filter (predC1 x) s.
+Proof.
+elim: s => //= y s IHs /andP[not_s_y /IHs->].
+by case: eqP => //= <-; apply/esym/all_filterP; rewrite all_predC has_pred1.
+Qed.
+
+Lemma mem_rem_uniq s : uniq s -> rem s =i [predD1 s & x].
+Proof. by move/rem_filter=> -> y; rewrite mem_filter. Qed.
+
+End Rem.
+
+Section Map.
+
+Variables (n0 : nat) (T1 : Type) (x1 : T1).
+Variables (T2 : Type) (x2 : T2) (f : T1 -> T2).
+
+Fixpoint map s := if s is x :: s' then f x :: map s' else [::].
+
+Lemma map_cons x s : map (x :: s) = f x :: map s.
+Proof. by []. Qed.
+
+Lemma map_nseq x : map (nseq n0 x) = nseq n0 (f x).
+Proof. by elim: n0 => // *; congr (_ :: _). Qed.
+
+Lemma map_cat s1 s2 : map (s1 ++ s2) = map s1 ++ map s2.
+Proof. by elim: s1 => [|x s1 IHs] //=; rewrite IHs. Qed.
+
+Lemma size_map s : size (map s) = size s.
+Proof. by elim: s => //= x s ->. Qed.
+
+Lemma behead_map s : behead (map s) = map (behead s).
+Proof. by case: s. Qed.
+
+Lemma nth_map n s : n < size s -> nth x2 (map s) n = f (nth x1 s n).
+Proof. by elim: s n => [|x s IHs] [|n]; try exact (IHs n). Qed.
+
+Lemma map_rcons s x : map (rcons s x) = rcons (map s) (f x).
+Proof. by rewrite -!cats1 map_cat. Qed.
+
+Lemma last_map s x : last (f x) (map s) = f (last x s).
+Proof. by elim: s x => /=. Qed.
+
+Lemma belast_map s x : belast (f x) (map s) = map (belast x s).
+Proof. by elim: s x => //= y s IHs x; rewrite IHs. Qed.
+
+Lemma filter_map a s : filter a (map s) = map (filter (preim f a) s).
+Proof. by elim: s => //= x s IHs; rewrite (fun_if map) /= IHs. Qed.
+
+Lemma find_map a s : find a (map s) = find (preim f a) s.
+Proof. by elim: s => //= x s ->. Qed.
+
+Lemma has_map a s : has a (map s) = has (preim f a) s.
+Proof. by elim: s => //= x s ->. Qed.
+
+Lemma all_map a s : all a (map s) = all (preim f a) s.
+Proof. by elim: s => //= x s ->. Qed.
+
+Lemma count_map a s : count a (map s) = count (preim f a) s.
+Proof. by elim: s => //= x s ->. Qed.
+
+Lemma map_take s : map (take n0 s) = take n0 (map s).
+Proof. by elim: n0 s => [|n IHn] [|x s] //=; rewrite IHn. Qed.
+
+Lemma map_drop s : map (drop n0 s) = drop n0 (map s).
+Proof. by elim: n0 s => [|n IHn] [|x s] //=; rewrite IHn. Qed.
+
+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.
+
+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.
+
+Lemma map_mask m s : map (mask m s) = mask m (map s).
+Proof. by elim: m s => [|[|] m IHm] [|x p] //=; rewrite IHm. Qed.
+
+Lemma inj_map : injective f -> injective map.
+Proof.
+by move=> injf; elim=> [|y1 s1 IHs] [|y2 s2] //= [/injf-> /IHs->].
+Qed.
+
+End Map.
+
+Notation "[ 'seq' E | i <- s ]" := (map (fun i => E) s)
+  (at level 0, E at level 99, i ident,
+   format "[ '[hv' 'seq'  E '/ '  |  i  <-  s ] ']'") : seq_scope.
+
+Notation "[ 'seq' E | i <- s & C ]" := [seq E | i <- [seq i <- s | C]]
+  (at level 0, E at level 99, i ident,
+   format "[ '[hv' 'seq'  E '/ '  |  i  <-  s '/ '  &  C ] ']'") : seq_scope.
+
+Notation "[ 'seq' E | i : T <- s ]" := (map (fun i : T => E) s)
+  (at level 0, E at level 99, i ident, only parsing) : seq_scope.
+
+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.
+
+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.
+
+Section FilterSubseq.
+
+Variable T : eqType.
+Implicit Types (s : seq T) (a : pred T).
+
+Lemma filter_subseq a s : subseq (filter a s) s.
+Proof. by apply/subseqP; exists (map a s); rewrite ?size_map ?filter_mask. Qed.
+
+Lemma subseq_filter s1 s2 a :
+  subseq s1 (filter a s2) = all a s1 && subseq s1 s2.
+Proof.
+elim: s2 s1 => [|x s2 IHs] [|y s1] //=; rewrite ?andbF ?sub0seq //.
+by case a_x: (a x); rewrite /= !IHs /=; case: eqP => // ->; rewrite a_x.
+Qed.
+
+Lemma subseq_uniqP s1 s2 :
+  uniq s2 -> reflect (s1 = filter (mem s1) s2) (subseq 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.
+by rewrite mem_filter; apply: andb_idr; exact: (mem_subseq ss12).
+Qed.
+
+Lemma perm_to_subseq s1 s2 :
+  subseq s1 s2 -> {s3 | perm_eq s2 (s1 ++ s3)}.
+Proof.
+elim Ds2: s2 s1 => [|y s2' IHs] [|x s1] //=; try by exists s2; rewrite Ds2.
+case: eqP => [-> | _] /IHs[s3 perm_s2] {IHs}.
+  by exists s3; rewrite perm_cons.
+by exists (rcons s3 y); rewrite -cat_cons -perm_rcons -!cats1 catA perm_cat2r.
+Qed.
+
+End FilterSubseq.
+
+Implicit Arguments subseq_uniqP [T s1 s2].
+
+Section EqMap.
+
+Variables (n0 : nat) (T1 : eqType) (x1 : T1).
+Variables (T2 : eqType) (x2 : T2) (f : T1 -> T2).
+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]; [exact: predU1l | apply: predU1r; auto].
+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 exact: predU1r.
+by move: Dy Hxy => ->; case/predU1P: Hx' => [->|]; [rewrite eqxx | exists x'].
+Qed.
+
+Lemma map_uniq s : uniq (map f s) -> uniq s.
+Proof.
+elim: s => //= x s IHs /andP[not_sfx /IHs->]; rewrite andbT.
+by apply: contra not_sfx => sx; apply/mapP; exists x.
+Qed.
+
+Lemma map_inj_in_uniq s : {in s &, injective f} -> uniq (map f s) = uniq s.
+Proof.
+elim: s => //= x s IHs //= injf; congr (~~ _ && _).
+  apply/mapP/idP=> [[y sy /injf] | ]; last by exists x.
+  by rewrite mem_head mem_behead // => ->.
+apply: IHs => y z sy sz; apply: injf => //; exact: predU1r.
+Qed.
+
+Lemma map_subseq s1 s2 : subseq s1 s2 -> subseq (map f s1) (map f s2).
+Proof.
+case/subseqP=> m sz_m ->; apply/subseqP.
+by exists m; rewrite ?size_map ?map_mask.
+Qed.
+
+Lemma nth_index_map s x0 x :
+  {in s &, injective f} -> x \in s -> nth x0 s (index (f x) (map f s)) = x.
+Proof.
+elim: s => //= y s IHs inj_f s_x; rewrite (inj_in_eq inj_f) ?mem_head //.
+move: s_x; rewrite inE eq_sym; case: eqP => [-> | _] //=; apply: IHs.
+by apply: sub_in2 inj_f => z; exact: 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.
+
+Hypothesis Hf : injective f.
+
+Lemma mem_map s x : (f x \in map f s) = (x \in s).
+Proof. by apply/mapP/idP=> [[y Hy /Hf->] //|]; exists x. Qed.
+
+Lemma index_map s x : index (f x) (map f s) = index x s.
+Proof. by rewrite /index; elim: s => //= y s IHs; rewrite (inj_eq Hf) IHs. Qed.
+
+Lemma map_inj_uniq s : uniq (map f s) = uniq s.
+Proof. apply: map_inj_in_uniq; exact: in2W. Qed.
+
+End EqMap.
+
+Implicit Arguments mapP [T1 T2 f s y].
+Prenex Implicits mapP.
+
+Lemma map_of_seq (T1 : eqType) T2 (s : seq T1) (fs : seq T2) (y0 : T2) :
+  {f | uniq s -> size fs = size s -> map f s = fs}.
+Proof.
+exists (fun x => nth y0 fs (index x s)) => uAs eq_sz.
+apply/esym/(@eq_from_nth _ y0); rewrite ?size_map eq_sz // => i ltis.
+have x0 : T1 by [case: (s) ltis]; by rewrite (nth_map x0) // index_uniq.
+Qed.
+
+Section MapComp.
+
+Variable T1 T2 T3 : Type.
+
+Lemma map_id (s : seq T1) : map id s = s.
+Proof. by elim: s => //= x s ->. Qed.
+
+Lemma eq_map (f1 f2 : T1 -> T2) : f1 =1 f2 -> map f1 =1 map f2.
+Proof. by move=> Ef; elim=> //= x s ->; rewrite Ef. Qed.
+
+Lemma map_comp (f1 : T2 -> T3) (f2 : T1 -> T2) s :
+  map (f1 \o f2) s = map f1 (map f2 s).
+Proof. by elim: s => //= x s ->. Qed.
+
+Lemma mapK (f1 : T1 -> T2) (f2 : T2 -> T1) :
+  cancel f1 f2 -> cancel (map f1) (map f2).
+Proof. by move=> eq_f12; elim=> //= x s ->; rewrite eq_f12. Qed.
+
+End MapComp.
+
+Lemma eq_in_map (T1 : eqType) T2 (f1 f2 : T1 -> T2) (s : seq T1) :
+  {in s, f1 =1 f2} <-> map f1 s = map f2 s.
+Proof.
+elim: s => //= x s IHs; split=> [eqf12 | [f12x /IHs eqf12]]; last first.
+  by move=> y /predU1P[-> | /eqf12].
+rewrite eqf12 ?mem_head //; congr (_ :: _).
+by apply/IHs=> y s_y; rewrite eqf12 // mem_behead.
+Qed.
+
+Lemma map_id_in (T : eqType) f (s : seq T) : {in s, f =1 id} -> map f s = s.
+Proof. by move/eq_in_map->; apply: map_id. Qed.
+
+(* Map a partial function *)
+
+Section Pmap.
+
+Variables (aT rT : Type) (f : aT -> option rT) (g : rT -> aT).
+
+Fixpoint pmap s :=
+  if s is x :: s' then let r := pmap s' in oapp (cons^~ r) r (f x) else [::].
+
+Lemma map_pK : pcancel g f -> cancel (map g) pmap.
+Proof. by move=> gK; elim=> //= x s ->; rewrite gK. Qed.
+
+Lemma size_pmap s : size (pmap s) = count [eta f] s.
+Proof. by elim: s => //= x s <-; case: (f _). Qed.
+
+Lemma pmapS_filter s : map some (pmap s) = map f (filter [eta f] s).
+Proof. by elim: s => //= x s; case fx: (f x) => //= [u] <-; congr (_ :: _). Qed.
+
+Hypothesis fK : ocancel f g.
+
+Lemma pmap_filter s : map g (pmap s) = filter [eta f] s.
+Proof. by elim: s => //= x s <-; rewrite -{3}(fK x); case: (f _). Qed.
+
+End Pmap.
+
+Section EqPmap.
+
+Variables (aT rT : eqType) (f : aT -> option rT) (g : rT -> aT).
+
+Lemma eq_pmap (f1 f2 : aT -> option rT) : f1 =1 f2 -> pmap f1 =1 pmap f2.
+Proof. by move=> Ef; elim=> //= x s ->; rewrite Ef. Qed.
+
+Lemma mem_pmap s u : (u \in pmap f s) = (Some u \in map f s).
+Proof. by elim: s => //= x s IHs; rewrite in_cons -IHs; case: (f x). Qed.
+
+Hypothesis fK : ocancel f g.
+
+Lemma can2_mem_pmap : pcancel g f -> forall s u, (u \in pmap f s) = (g u \in s).
+Proof.
+by move=> gK s u; rewrite -(mem_map (pcan_inj gK)) pmap_filter // mem_filter gK.
+Qed.
+
+Lemma pmap_uniq s : uniq s -> uniq (pmap f s).
+Proof.
+by move/(filter_uniq [eta f]); rewrite -(pmap_filter fK); exact: map_uniq.
+Qed.
+
+End EqPmap.
+
+Section PmapSub.
+
+Variables (T : Type) (p : pred T) (sT : subType p).
+
+Lemma size_pmap_sub s : size (pmap (insub : T -> option sT) s) = count p s.
+Proof. by rewrite size_pmap (eq_count (isSome_insub _)). Qed.
+
+End PmapSub.
+
+Section EqPmapSub.
+
+Variables (T : eqType) (p : pred T) (sT : subType p).
+
+Let insT : T -> option sT := insub.
+
+Lemma mem_pmap_sub s u : (u \in pmap insT s) = (val u \in s).
+Proof. apply: (can2_mem_pmap (insubK _)); exact: valK. Qed.
+
+Lemma pmap_sub_uniq s : uniq s -> uniq (pmap insT s).
+Proof. exact: (pmap_uniq (insubK _)). Qed.
+
+End EqPmapSub.
+
+(* Index sequence *)
+
+Fixpoint iota m n := if n is n'.+1 then m :: iota m.+1 n' else [::].
+
+Lemma size_iota m n : size (iota m n) = n.
+Proof. by elim: n m => //= n IHn m; rewrite IHn. Qed.
+
+Lemma iota_add m n1 n2 : iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2.
+Proof.
+by elim: n1 m => //= [|n1 IHn1] m; rewrite ?addn0 // -addSnnS -IHn1.
+Qed.
+
+Lemma iota_addl m1 m2 n : iota (m1 + m2) n = map (addn m1) (iota m2 n).
+Proof. by elim: n m2 => //= n IHn m2; rewrite -addnS IHn. Qed.
+
+Lemma nth_iota m n i : i < n -> nth 0 (iota m n) i = m + i.
+Proof.
+by move/subnKC <-; rewrite addSnnS iota_add nth_cat size_iota ltnn subnn.
+Qed.
+
+Lemma mem_iota m n i : (i \in iota m n) = (m <= i) && (i < m + n).
+Proof.
+elim: n m => [|n IHn] /= m; first by rewrite addn0 ltnNge andbN.
+rewrite -addSnnS leq_eqVlt in_cons eq_sym.
+by case: eqP => [->|_]; [rewrite leq_addr | exact: IHn].
+Qed.
+
+Lemma iota_uniq m n : uniq (iota m n).
+Proof. by elim: n m => //= n IHn m; rewrite mem_iota ltnn /=. Qed.
+
+(* Making a sequence of a specific length, using indexes to compute items. *)
+
+Section MakeSeq.
+
+Variables (T : Type) (x0 : T).
+
+Definition mkseq f n : seq T := map f (iota 0 n).
+
+Lemma size_mkseq f n : size (mkseq f n) = n.
+Proof. by rewrite size_map size_iota. Qed.
+
+Lemma eq_mkseq f g : f =1 g -> mkseq f =1 mkseq g.
+Proof. by move=> Efg n; exact: eq_map Efg _. Qed.
+
+Lemma nth_mkseq f n i : i < n -> nth x0 (mkseq f n) i = f i.
+Proof. by move=> Hi; rewrite (nth_map 0) ?nth_iota ?size_iota. Qed.
+
+Lemma mkseq_nth s : mkseq (nth x0 s) (size s) = s.
+Proof.
+by apply: (@eq_from_nth _ x0); rewrite size_mkseq // => i Hi; rewrite nth_mkseq.
+Qed.
+
+End MakeSeq.
+
+Section MakeEqSeq.
+
+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)) :
+  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.
+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.
+by rewrite map_rotr /= -map_comp -(@eq_map _ _ (nth x0 t)) // -Ds1 -Ds rotK.
+Qed.
+
+End MakeEqSeq.
+
+Implicit Arguments perm_eq_iotaP [[T] [s] [t]].
+
+Section FoldRight.
+
+Variables (T : Type) (R : Type) (f : T -> R -> R) (z0 : R).
+
+Fixpoint foldr s := if s is x :: s' then f x (foldr s') else z0.
+
+End FoldRight.
+
+Section FoldRightComp.
+
+Variables (T1 T2 : Type) (h : T1 -> T2).
+Variables (R : Type) (f : T2 -> R -> R) (z0 : R).
+
+Lemma foldr_cat s1 s2 : foldr f z0 (s1 ++ s2) = foldr f (foldr f z0 s2) s1.
+Proof. by elim: s1 => //= x s1 ->. Qed.
+
+Lemma foldr_map s : foldr f z0 (map h s) = foldr (fun x z => f (h x) z) z0 s.
+Proof. by elim: s => //= x s ->. Qed.
+
+End FoldRightComp.
+
+(* Quick characterization of the null sequence. *)
+
+Definition sumn := foldr addn 0.
+
+Lemma sumn_nseq x n : sumn (nseq n x) = x * n.
+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 natnseq0P s : reflect (s = nseq (size s) 0) (sumn s == 0).
+Proof.
+apply: (iffP idP) => [|->]; last by rewrite sumn_nseq.
+by elim: s => //= x s IHs; rewrite addn_eq0 => /andP[/eqP-> /IHs <-].
+Qed.
+
+Section FoldLeft.
+
+Variables (T R : Type) (f : R -> T -> R).
+
+Fixpoint foldl z s := if s is x :: s' then foldl (f z x) s' else z.
+
+Lemma foldl_rev z s : foldl z (rev s) = foldr (fun x z => f z x) z s.
+Proof.
+elim/last_ind: s z => [|s x IHs] z //=.
+by rewrite rev_rcons -cats1 foldr_cat -IHs.
+Qed.
+
+Lemma foldl_cat z s1 s2 : foldl z (s1 ++ s2) = foldl (foldl z s1) s2.
+Proof.
+by rewrite -(revK (s1 ++ s2)) foldl_rev rev_cat foldr_cat -!foldl_rev !revK.
+Qed.
+
+End FoldLeft.
+
+Section Scan.
+
+Variables (T1 : Type) (x1 : T1) (T2 : Type) (x2 : T2).
+Variables (f : T1 -> T1 -> T2) (g : T1 -> T2 -> T1).
+
+Fixpoint pairmap x s := if s is y :: s' then f x y :: pairmap y s' else [::].
+
+Lemma size_pairmap x s : size (pairmap x s) = size s.
+Proof. by elim: s x => //= y s IHs x; rewrite IHs. Qed.
+
+Lemma pairmap_cat x s1 s2 :
+  pairmap x (s1 ++ s2) = pairmap x s1 ++ pairmap (last x s1) s2.
+Proof. by elim: s1 x => //= y s1 IHs1 x; rewrite IHs1. Qed.
+
+Lemma nth_pairmap s n : n < size s ->
+  forall x, nth x2 (pairmap x s) n = f (nth x1 (x :: s) n) (nth x1 s n).
+Proof. by elim: s n => [|y s IHs] [|n] //= Hn x; apply: IHs. Qed.
+
+Fixpoint scanl x s :=
+  if s is y :: s' then let x' := g x y in x' :: scanl x' s' else [::].
+
+Lemma size_scanl x s : size (scanl x s) = size s.
+Proof. by elim: s x => //= y s IHs x; rewrite IHs. Qed.
+
+Lemma scanl_cat x s1 s2 :
+  scanl x (s1 ++ s2) = scanl x s1 ++ scanl (foldl g x s1) s2.
+Proof. by elim: s1 x => //= y s1 IHs1 x; rewrite IHs1. Qed.
+
+Lemma nth_scanl s n : n < size s ->
+  forall x, nth x1 (scanl x s) n = foldl g x (take n.+1 s).
+Proof. by elim: s n => [|y s IHs] [|n] Hn x //=; rewrite ?take0 ?IHs. Qed.
+
+Lemma scanlK :
+  (forall x, cancel (g x) (f x)) -> forall x, cancel (scanl x) (pairmap x).
+Proof. by move=> Hfg x s; elim: s x => //= y s IHs x; rewrite Hfg IHs. Qed.
+
+Lemma pairmapK :
+  (forall x, cancel (f x) (g x)) -> forall x, cancel (pairmap x) (scanl x).
+Proof. by move=> Hgf x s; elim: s x => //= y s IHs x; rewrite Hgf IHs. Qed.
+
+End Scan.
+
+Prenex Implicits mask map pmap foldr foldl scanl pairmap.
+
+Section Zip.
+
+Variables S T : Type.
+
+Fixpoint zip (s : seq S) (t : seq T) {struct t} :=
+  match s, t with
+  | x :: s', y :: t' => (x, y) :: zip s' t'
+  | _, _ => [::]
+  end.
+
+Definition unzip1 := map (@fst S T).
+Definition unzip2 := map (@snd S T).
+
+Lemma zip_unzip s : zip (unzip1 s) (unzip2 s) = s.
+Proof. by elim: s => [|[x y] s /= ->]. Qed.
+
+Lemma unzip1_zip s t : size s <= size t -> unzip1 (zip s t) = s.
+Proof. by elim: s t => [|x s IHs] [|y t] //= le_s_t; rewrite IHs. Qed.
+
+Lemma unzip2_zip s t : size t <= size s -> unzip2 (zip s t) = t.
+Proof. by elim: s t => [|x s IHs] [|y t] //= le_t_s; rewrite IHs. Qed.
+
+Lemma size1_zip s t : size s <= size t -> size (zip s t) = size s.
+Proof. by elim: s t => [|x s IHs] [|y t] //= Hs; rewrite IHs. Qed.
+
+Lemma size2_zip s t : size t <= size s -> size (zip s t) = size t.
+Proof. by elim: s t => [|x s IHs] [|y t] //= Hs; rewrite IHs. Qed.
+
+Lemma size_zip s t : size (zip s t) = minn (size s) (size t).
+Proof.
+by elim: s t => [|x s IHs] [|t2 t] //=; rewrite IHs -add1n addn_minr.
+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.
+
+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).
+Proof. by elim: i s t => [|i IHi] [|y1 s1] [|y2 t] //= [/IHi->]. Qed.
+
+Lemma nth_zip_cond p s t i :
+   nth p (zip s t) i
+     = (if i < size (zip s t) then (nth p.1 s i, nth p.2 t i) else p).
+Proof.
+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).
+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).
+Proof.
+elim: s1 s2 => [|x s1 IHs] [|y s2] //= [eq_sz].
+by rewrite !rev_cons zip_rcons ?IHs ?size_rev.
+Qed.
+
+End Zip.
+
+Prenex Implicits zip unzip1 unzip2.
+
+Section Flatten.
+
+Variable T : Type.
+Implicit Types (s : seq T) (ss : seq (seq T)).
+
+Definition flatten := foldr cat (Nil T).
+Definition shape := map (@size T).
+Fixpoint reshape sh s :=
+  if sh is n :: sh' then take n s :: reshape sh' (drop n s) else [::].
+
+Lemma size_flatten ss : size (flatten ss) = sumn (shape ss).
+Proof. by elim: ss => //= s ss <-; rewrite size_cat. Qed.
+
+Lemma flatten_cat ss1 ss2 :
+  flatten (ss1 ++ ss2) = flatten ss1 ++ flatten ss2.
+Proof. by elim: ss1 => //= s ss1 ->; rewrite catA. Qed.
+
+Lemma flattenK ss : reshape (shape ss) (flatten ss) = ss.
+Proof.
+by elim: ss => //= s ss IHss; rewrite take_size_cat ?drop_size_cat ?IHss.
+Qed.
+
+Lemma reshapeKr sh s : size s <= sumn sh -> flatten (reshape sh s) = s.
+Proof.
+elim: sh s => [[]|n sh IHsh] //= s sz_s; rewrite IHsh ?cat_take_drop //.
+by rewrite size_drop leq_subLR.
+Qed.
+
+Lemma reshapeKl sh s : size s >= sumn sh -> shape (reshape sh s) = sh.
+Proof.
+elim: sh s => [[]|n sh IHsh] //= s sz_s.
+rewrite size_takel; last exact: leq_trans (leq_addr _ _) sz_s.
+by rewrite IHsh // -(leq_add2l n) size_drop -maxnE leq_max sz_s orbT.
+Qed.
+
+End Flatten.
+
+Prenex Implicits flatten shape reshape.
+
+Section EqFlatten.
+
+Variables S T : eqType.
+
+Lemma flattenP (A : seq (seq T)) x :
+  reflect (exists2 s, s \in A & x \in s) (x \in flatten A).
+Proof.
+elim: A => /= [|s A /iffP IH_A]; [by right; case | rewrite mem_cat].
+have [s_x|s'x] := @idP (x \in s); first by left; exists s; rewrite ?mem_head.
+by apply: IH_A => [[t] | [t /predU1P[->|]]]; exists t; rewrite // mem_behead.
+Qed.
+Implicit Arguments flattenP [A x].
+
+Lemma flatten_mapP (A : S -> seq T) s y :
+  reflect (exists2 x, x \in s & y \in A x) (y \in flatten (map A s)).
+Proof.
+apply: (iffP flattenP) => [[_ /mapP[x sx ->]] | [x sx]] Axy; first by exists x.
+by exists (A x); rewrite ?map_f.
+Qed.
+
+End EqFlatten.
+
+Implicit Arguments flattenP [T A x].
+Implicit 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.
+
+Section AllPairs.
+
+Variables (S T R : Type) (f : S -> T -> R).
+Implicit Types (s : seq S) (t : seq T).
+
+Definition allpairs s t := foldr (fun x => cat (map (f x) t)) [::] s.
+
+Lemma size_allpairs s t : size (allpairs s t) = size s * size t.
+Proof. by elim: s => //= x s IHs; rewrite size_cat size_map IHs. Qed.
+
+Lemma allpairs_cat s1 s2 t :
+  allpairs (s1 ++ s2) t = allpairs s1 t ++ allpairs s2 t.
+Proof. by elim: s1 => //= x s1 ->; rewrite catA. Qed.
+
+End AllPairs.
+
+Prenex Implicits allpairs.
+
+Notation "[ 'seq' E | i <- s , j <- t ]" := (allpairs (fun i j => E) s t)
+  (at level 0, E at level 99, i ident, j ident,
+   format "[ '[hv' 'seq'  E '/ '  |  i  <-  s , '/   '  j  <-  t ] ']'")
+   : seq_scope.
+Notation "[ 'seq' E | i : T <- s , j : U <- t ]" :=
+  (allpairs (fun (i : T) (j : U) => E) s t)
+  (at level 0, E at level 99, i ident, j ident, only parsing) : seq_scope.
+
+Section EqAllPairs.
+
+Variables S T : eqType.
+Implicit Types (R : eqType) (s : seq S) (t : seq T).
+
+Lemma allpairsP R (f : S -> T -> R) s t z :
+  reflect (exists p, [/\ p.1 \in s, p.2 \in t & z = f p.1 p.2])
+          (z \in allpairs f s t).
+Proof.
+elim: s => [|x s IHs /=]; first by right=> [[p []]].
+rewrite mem_cat; have [fxt_z | not_fxt_z] := altP mapP.
+  by left; have [y t_y ->] := fxt_z; exists (x, y); rewrite mem_head.
+apply: (iffP IHs) => [] [[x' y] /= [s_x' t_y def_z]]; exists (x', y).
+  by rewrite !inE predU1r.
+by have [def_x' | //] := predU1P s_x'; rewrite def_z def_x' map_f in not_fxt_z.
+Qed.
+
+Lemma mem_allpairs R (f : S -> T -> R) s1 t1 s2 t2 :
+  s1 =i s2 -> t1 =i t2 -> allpairs f s1 t1 =i allpairs f s2 t2.
+Proof.
+move=> eq_s eq_t z.
+by apply/allpairsP/allpairsP=> [] [p fpz]; exists p; rewrite eq_s eq_t in fpz *.
+Qed.
+
+Lemma allpairs_catr R (f : S -> T -> R) s t1 t2 :
+  allpairs f s (t1 ++ t2) =i allpairs f s t1 ++ allpairs f s t2.
+Proof.
+move=> z; rewrite mem_cat.
+apply/allpairsP/orP=> [[p [sP1]]|].
+  by rewrite mem_cat; case/orP; [left | right]; apply/allpairsP; exists p.
+by case=> /allpairsP[p [sp1 sp2 ->]]; exists p; rewrite mem_cat sp2 ?orbT.
+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)} ->
+  uniq (allpairs f s t).
+Proof.
+move=> Us Ut inj_f; have: all (mem s) s by exact/allP.
+elim: {-2}s Us => //= x s1 IHs /andP[s1'x Us1] /andP[sx1 ss1].
+rewrite cat_uniq {}IHs // andbT map_inj_in_uniq ?Ut // => [|y1 y2 *].
+  apply/hasPn=> _ /allpairsP[z [s1z tz ->]]; apply/mapP=> [[y ty Dy]].
+  suffices [Dz1 _]: (z.1, z.2) = (x, y) by rewrite -Dz1 s1z in s1'x.
+  apply: inj_f => //; apply/allpairsP; last by exists (x, y).
+  by have:= allP ss1 _ s1z; exists z.
+suffices: (x, y1) = (x, y2) by case.
+by apply: inj_f => //; apply/allpairsP; [exists (x, y1) | exists (x, y2)].
+Qed.
+
+End EqAllPairs.