(*****************************************************************************)
(* Copyright 2022 TheWalker77                                                *)
(* Permutations: Copyright 2017 IMDEA Software Institute                     *)
(*                                                                           *)
(* Licensed under the Apache License, Version 2.0 (the "License");           *)
(* you may not use this file except in compliance with the License.          *)
(* You may obtain a copy of the License at                                   *)
(*                                                                           *)
(*     http://www.apache.org/licenses/LICENSE-2.0                            *)
(*                                                                           *)
(* Unless required by applicable law or agreed to in writing, software       *)
(* distributed under the License is distributed on an "AS IS" BASIS,         *)
(* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.  *)
(* See the License for the specific language governing permissions and       *)
(* limitations under the License.                                            *)
(*****************************************************************************)

From mathcomp Require Export all_ssreflect zify.
From mathcomp Require Export seq.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

Lemma rcons_to_cat T (s: seq T) a: rcons s a = s ++ a::[::].
Proof.
elim: s => [//|a' s IH] /=.
by rewrite IH.
Qed.

Lemma map_cat_id T (s1 s2: seq T) f: map f (s1 ++ s2) = s1 ++ s2 ->
    map f s1 = s1 /\ map f s2 = s2.
Proof.
elim: s1 s2 => [|t s1 IHs1] s2 //=.
by move => [-> /IHs1 [-> ->]].
Qed.

Lemma size_zero_iff_nil {A} (s: seq A):
    size s = 0 <-> s = [::].
Proof.
by case :s.
Qed.
Lemma zip_emptyl {A B} (s: seq B): @zip A B [::] s = [::].
Proof.
by case: s.
Qed.

Lemma zip_emptyr {A B} (s: seq A): @zip A B s [::] = [::].
Proof.
by case: s.
Qed.

Lemma map_zip2 {A B C D} (s1: seq A) (s2: seq B) (f: A -> C) (g: B -> D):
    zip (map f s1) (map g s2) = map (fun xy => ((f (fst xy)), (g (snd xy)))) (zip s1 s2).
Proof.
elim: s2 s1 => [|b s2 IHs2];
    elim => [|a s1 IHs1] //=.
by rewrite IHs2.
Qed.

Lemma zip_rcons {A B} (a: A) (b: B) sa sb:
    size sa = size sb ->
    zip (rcons sa a) (rcons sb b) = rcons (zip sa sb) (a, b).
Proof.
elim: sa sb a b => [/=|a' sa IHsa] [|b' sb] a b //=.
move => [Hsize].
by rewrite IHsa.
Qed.

(* propositional version of \in this one does not require eqTypev*)
Inductive PIn {A}: A -> seq A -> Prop :=
| pin_here (a : A) l : PIn a (a::l)
| pin_future (a b : A) l : PIn a l -> PIn a (b::l).

Lemma inP (A: eqType): forall (a: A) (l: seq A),  reflect (PIn a l) (a \in l).
Proof.
move => a l.
apply: (iffP idP).
-   move: a.
    have ? := pin_here.
    elim : l  => [|a' l Hind] //= a /[!in_cons].
    move /orP => [|a_in_l].
        by move /eqP ->.
    apply: pin_future.
    by apply: Hind.
-   move => HPIn.
    induction HPIn as [a l| a b l HInd].
        by apply: mem_head.
    rewrite in_cons.
    apply/orP.
    by right.
Qed.

Lemma neg_inP (A: eqType): forall (a: A) (l: seq A),
    reflect (~ PIn a l) (a \notin l).
Proof.
move => a l.
apply: (iffP idP).
-   move /negP => a_not_in_l a_PIn_l.
    apply: a_not_in_l.
    by apply/inP.
-   move => not_PIn_a_l.
    apply/negP => a_in_l.
    apply: not_PIn_a_l.
    by apply/inP.
Qed.

Lemma PIn_cons_or A (a b: A) (l: seq A) : PIn a (b::l) <->
    a = b \/ PIn a l.
Proof.
split.
    move => HPIn.
    inversion HPIn; subst.
        by left.
    by right.
move => [-> | HPIn].
    by apply: pin_here.
by apply: pin_future.
Qed.

Lemma not_PIn_cons_and A (a b: A) (l: seq A) : ~ PIn a (b::l) <->
    a <> b /\ ~ PIn a l.
Proof.
rewrite PIn_cons_or.
split.
    move => Hnot.
    split;
        move => HFalse;
        apply: Hnot.
        by left.
    by right.
by move => [Hneq HnotIn] [Heq | Hin].
Qed.

Lemma PIn_empty_false A (a: A): ~ PIn a [::].
Proof.
move =>HFalse.
inversion HFalse.
Qed.

Lemma PIn_empty_false_iff A (a: A): PIn a [::] <-> False.
Proof.
split.
    by apply: PIn_empty_false.
by [].
Qed.

Lemma PIn_empty A (l: seq A) : l = [::] <-> forall a, ~PIn a l.
Proof.
split.
    move ->.
    by apply: PIn_empty_false.
case : l => [|a l] Hnot_in.
    by [].
have HFalse := (Hnot_in a).
contradict HFalse.
by apply: pin_here.
Qed.

Lemma PIn_here_eq A (a b: A) (l: seq A): a = b -> PIn a (b::l).
Proof.
move ->.
by apply: pin_here.
Qed.

Lemma pin_map1 {A B } (b: B) (l : seq A) f:
    PIn b (map f l) -> exists a, b = f a /\ PIn a l.
Proof.
elim : l => [|a l IHl] /=.
        move => HFalse.
        by inversion HFalse.
move /PIn_cons_or => [->|pin_l].
    exists a.
    split.
        by [].
    apply: pin_here.
case : (IHl pin_l) => [a' [-> Hin]].
exists a'.
split.
    by [].
by apply: pin_future.
Qed.

Lemma pin_map2 {A B} (b: B) (l : seq A) f:
    (exists a, b = f a /\ PIn a l) -> PIn b (map f l).
Proof.
elim : l => [| a l IHl] /=;
    move => [a' []].
    by rewrite !PIn_empty_false_iff.
move => Heq.
move : Heq IHl => -> IHl.
move /PIn_cons_or => [->|Hin].
    by apply: pin_here.
apply: pin_future.
apply: IHl.
by exists a'.
Qed.

Lemma pin_map {A B } (b: B) (l : seq A) f:
    PIn b (map f l) <-> exists a, b = f a /\ PIn a l.
Proof.
split.
    by apply: pin_map1.
by apply: pin_map2.
Qed.


Lemma pin_seq_pin_fst A B (l: seq (A * B)) k v:
    PIn (k, v) l ->
    PIn k (map (fun kv => kv.1) l).
Proof.
elim : l => [| [k' v'] l IHl] /=.
    by rewrite !PIn_empty_false_iff.
move /PIn_cons_or => [[<- Heq]| Hin].
    by apply: pin_here.
apply: pin_future.
by apply: IHl.
Qed.

Lemma PIn_app A a (l1 l2: seq A) : PIn a (l1 ++ l2) <-> PIn a l1 \/ PIn a l2.
Proof.
elim : l1 => [|a' l1 IHl1] /=.
    split.
        by right.
    move => [HFalse | HIn];
        by [|have := PIn_empty_false HFalse].
rewrite !PIn_cons_or IHl1.
split.
    move => [->|[Hin|Hin]].
    -   left.
        by left.
    -   left.
        by right.
    -   by right.
move => [[->|Hin]|Hin].
-   by left.
-   right.
    by left.
-   right.
    by right.
Qed.

Lemma PIn_singlton {A} (a b: A): a = b <-> PIn a [:: b].
Proof.
split.
    move ->.
    apply: pin_here.
rewrite PIn_cons_or.
move => [->|HFalse];
    by [| have := PIn_empty_false HFalse].
Qed.

Lemma PIn_rev A a (l: seq A) : PIn a l <-> PIn a (rev l).
Proof.
elim : l => [|a' l IHl].
    by rewrite /rev /=.
rewrite PIn_cons_or -cat1s.
by rewrite rev_cat PIn_app -PIn_singlton IHl or_comm.
Qed.

Lemma PIn_rcons_or A (a b: A) (l: seq A) : PIn a (rcons l b) <->
    a = b \/ PIn a l.
Proof.
rewrite PIn_rev rev_rcons PIn_cons_or.
by rewrite -PIn_rev.
Qed.

Lemma PIn_split1 A (a: A) l : PIn a l -> exists s1 s2, l = s1 ++ a :: s2.
Proof.
elim : l => [| a' l IHl].
    by rewrite PIn_empty_false_iff.
rewrite PIn_cons_or.
move => [<-| Hin].
    by exists [::], l.
move : (IHl Hin) => [s1 [s2 Heq]].
exists (a'::s1), s2.
by rewrite Heq.
Qed.

Lemma PIn_split2 A (a: A) l : (exists s1 s2, l = s1 ++ a :: s2) -> PIn a l.
Proof.
move => [s1 [s2 ->]].
rewrite PIn_app.
right.
by apply: pin_here.
Qed.

Lemma PIn_split A (a: A) l : PIn a l <-> exists s1 s2, l = s1 ++ a :: s2.
Proof.
split.
    by apply: PIn_split1.
by apply: PIn_split2.
Qed.

Lemma PIn_zip_id A (a b: A) l : PIn (a, b) (zip l l) <-> a = b /\ PIn a l.
Proof.
elim: l => [|a' l IHl] /=.
    rewrite !PIn_empty_false_iff.
    split => //.
    by move => [].
rewrite !PIn_cons_or IHl.
split.
    move => [[<- <-]|[<- ?]];
        split => //;
        by [left|right].
move => [<-] [<-|?];
    by [left | right].
Qed.

Lemma Pin_zip_flip A B (a: A) (b: B) la lb:
    PIn (a, b) (zip la lb) -> PIn (b, a) (zip lb la).
Proof.
elim: la lb a b => [|a' la IHla].
    move => ??? /=.
    by rewrite zip_emptyl PIn_empty_false_iff.
move => [|b' lb] a b /=.
    by rewrite PIn_empty_false_iff.
rewrite !PIn_cons_or.
move => [[-> ->]|Hin].
    by left.
right.
by apply: IHla.
Qed.

Lemma Pin_zip_flip_iff A B (a: A) (b: B) la lb:
    PIn (a, b) (zip la lb) <-> PIn (b, a) (zip lb la).
Proof.
split;
    by apply: Pin_zip_flip.
Qed.

Lemma seq_map_ext {A B } (l : seq A) (f g: A -> B):
    (forall x, PIn x l -> f x = g x) ->
    map f l = map g l.
Proof.
elim: l => [//|a l IHl] Hext /=.
rewrite Hext;
    last by apply: pin_here.
rewrite IHl //.
move => x Hin.
apply: Hext.
by apply: pin_future.
Qed.

(* propositional version of Uniq and it does not require eqType *)
Inductive PUniq {A} : seq A -> Prop :=
| puniq_nil : PUniq [::]
| puniq_cons (a: A) l: ~ PIn a l -> PUniq l -> PUniq (a::l).

Lemma uniqP (A: eqType): forall (l: seq A), reflect (PUniq l) (uniq l).
Proof.
move => l.
apply: (iffP idP).
-   have ? := puniq_nil.
    elim : l  => [|a l Hind] //=.
    move /andP => [a_not_in_l uniq_l].
    apply: puniq_cons.
        by apply/neg_inP.
    by apply: Hind.
-   move => HPuniq.
    induction HPuniq as [|a l a_not_in_l Hind] => //=.
    apply/andP.
    split => //=.
    by apply/neg_inP.
Qed.

Lemma uniq_inv A a (l: seq A):
    PUniq (a :: l) <->  ~ PIn a l /\ PUniq l.
Proof.
split.
    move => Huniq.
    by inversion Huniq; subst.
move => [Hnot_in Huniq].
by apply: puniq_cons.
Qed.

Lemma puniq_app1 A (s1 s2: seq A):
    PUniq (s1 ++ s2) ->
    PUniq s1 /\ PUniq s2 /\ (forall x, PIn x s1 -> PIn x s2 -> False).
Proof.
elim : s1 s2 => [|a s1 IHs1] s2 /=.
    move => Huniq2.
    split.
        by apply: puniq_nil.
    split.
        by [].
    move => x.
    by rewrite PIn_empty_false_iff.
rewrite !uniq_inv PIn_app.
move => [ Hnotin12 Huniq12].
move : (IHs1 _ Huniq12) => [Huniq1 [Huniq2 Hnotinin]].
split.
    split;
    last by [].
    move => Hina.
    apply Hnotin12.
    by left.
split.
    by [].
move => x.
rewrite PIn_cons_or.
move => [->|Hina1] Hina2.
    apply: Hnotin12.
    by right.
by apply: (Hnotinin x).
Qed.

Lemma puniq_app2 A (s1 s2: seq A):
    PUniq s1 ->
    PUniq s2 ->
    (forall x, PIn x s1 -> PIn x s2 -> False) ->
    PUniq (s1 ++ s2).
Proof.
elim : s1 s2 => [|a s1 IHs1] s2 /=.
    by [].
rewrite !uniq_inv.
move => [Hnotin1 Huniq1] Huni2 Hnotinin.
split.
    move /PIn_app => [Hin1|Hin2].
        by [].
    apply: (Hnotinin a).
        by apply: pin_here.
    by [].
apply: IHs1 => //=.
move => x Hin1 Hin2.
apply: (Hnotinin x);
    last by [].
rewrite PIn_cons_or.
by right.
Qed.

Lemma puniq_app A (s1 s2: seq A):
    PUniq (s1 ++ s2) <->
    PUniq s1 /\ PUniq s2 /\ (forall x, PIn x s1 -> PIn x s2 -> False).
Proof.
split.
    by apply: puniq_app1.
move => [?[]].
by apply: puniq_app2.
Qed.

Lemma puniq_map_inv_fun A B (l: seq A) (f: A -> B):
    (forall a b, PIn a l -> PIn b l -> f a = f b -> a = b) ->
    PUniq l -> PUniq (map f l).
Proof.
elim: l => [|a l IHl] /= Hinv.
    move => _.
    by apply: puniq_nil.
rewrite !uniq_inv.
move => [Hnotin Huniq].
split;
    last first.
    apply: IHl => // a' b' PIn Heq.
    apply: Hinv => //;
        by apply pin_future => //.
move /pin_map => [a' [Hfeq Hin]].
apply: Hnotin.
have := Hinv _ _ _ _ Hfeq.
move => -> //.
-   by apply pin_here.
-   by apply: pin_future.
Qed.

Lemma puniq_map_inv_fun_weak A B (l: seq A) (f: A -> B):
    (forall a b, f a = f b -> a = b) ->
    PUniq l -> PUniq (map f l).
Proof.
move => Hinj.
apply: puniq_map_inv_fun => a b Hina Hinb.
by apply: Hinj.
Qed.


(* properties of associated seqs *)
Lemma uniq_map_fst A B (l: seq (A * B)):
    (forall k v1 v2, PIn (k, v1) l -> PIn (k, v2) l -> v1 = v2) ->
    PUniq l -> PUniq (map (fun kv => kv.1) l).
Proof.
elim : l => [|[k v] l IHl] /= Hext Huniql /=.
    by apply: puniq_nil.
apply: puniq_cons;
    last first.
    apply: IHl;
        last by inversion Huniql.
    move => k' v1 v2 Hin1 Hin2.
    apply: (Hext k');
    by apply: pin_future.
move /pin_map => [[a b]] /= [] <- Hin.
inversion Huniql; subst.
have Hin_future: PIn (k,b) ((k, v)::l).
    by apply: pin_future.
have Hinkvl: PIn (k, v) ((k, v):: l).
    by apply: pin_here.
have Heq := Hext k b v Hin_future Hinkvl.
apply: H1.
by rewrite -Heq.
Qed.


Lemma uniq_map_in_in {A B} (l: seq (A * B)) k v1 v2:
    PUniq (map (fun kv => kv.1) l) ->
    PIn (k, v1) l ->
    PIn (k, v2) l ->
    v1 = v2.
Proof.
elim : l => [| [k' v'] l IHl] /=;
    rewrite ?PIn_empty_false_iff => Huniq Hinv1 Hinv2.
    by [].
move : Huniq.
move /uniq_inv => [Hnot_in Huniq].
move : Hinv1 Hinv2 Hnot_in IHl.
move /PIn_cons_or => [[<- <-]| Hin_v1];
    move /PIn_cons_or => [|].
-   by move => [<-].
-   move => Hin_v2 Hnot_in.
    by have := pin_seq_pin_fst  Hin_v2.
-   move => [<- ->] Hnot_in IHl.
    by have := pin_seq_pin_fst Hin_v1.
-   move => Hinv2 Hnot_in IHl.
    by apply: IHl.
Qed.

Definition seq_forall {A} (P: A -> Prop) (s: seq A) :=
    foldl (fun p a => P a /\ p ) True s.

Fixpoint seq_forall2 {A} (P: A -> Prop) (s: seq A) :=
match s with
| [::] => True
| a::s' => P a /\ seq_forall2 P s'
end.

Lemma all_seq_forall {A} P (s: seq A): all P s <-> seq_forall2 P s.
Proof.
elim: s => [//|a s IHs] /=.
rewrite -IHs.
split.
    by move/andP.
by move => [-> ->].
Qed.

Lemma seq_forall_forall {A} (P: A -> Prop) (s: seq A) :
    seq_forall P s <-> (forall a, PIn a s -> P a).
Proof.
rewrite /seq_forall.
elim/last_ind: s => [|l a IHl].
    split => //.
    move => _ a.
    by rewrite PIn_empty_false_iff.
rewrite foldl_rcons IHl.
split.
    move => [HP HIn] a'.
    move /PIn_rcons_or => [->|].
        by [].
    by apply: HIn.
move => HIn.
split.
    apply: HIn.
    apply/PIn_rcons_or.
    by left.
move => a' HInl.
apply: HIn.
apply/PIn_rcons_or.
by right.
Qed.

Lemma seq_forall2_forall {A} (P: A -> Prop) (s: seq A) :
seq_forall2 P s <-> (forall a, PIn a s -> P a).
Proof.
elim: s => [|a l IHl] /=.
    split => [_ a|//].
    by rewrite PIn_empty_false_iff.
split => [[Hp Hall] a'|].
    rewrite PIn_cons_or.
    move => [->//|].
    by apply IHl.
move => Hall.
split.
    apply Hall.
    rewrite PIn_cons_or.
    by left.
rewrite IHl => a' Hin.
apply Hall.
rewrite PIn_cons_or.
by right.
Qed.

Lemma seq_forall_seq_forall2 {A} (P: A -> Prop) (s: seq A) :
    seq_forall2 P s <-> seq_forall P s.
Proof.
by rewrite seq_forall2_forall seq_forall_forall.
Qed.

Lemma seq_forall_empty {A} (P: A -> Prop):
    seq_forall P [::] <-> True.
Proof.
rewrite seq_forall_forall.
split => [//|??].
by rewrite PIn_empty_false_iff.
Qed.

Definition seq_exists {A} (P: A -> Prop) (s: seq A) :=
    foldl (fun p a => P a \/ p ) False s.

Lemma seq_exists_exists {A} (P: A -> Prop) (s: seq A) :
    seq_exists P s <-> exists a, PIn a s /\ P a.
Proof.
rewrite /seq_exists.
elim/last_ind: s => [|s a IHs].
    split => //.
    move => [a []].
    by rewrite PIn_empty_false_iff.
rewrite foldl_rcons IHs.
split.
    move => [HP|[a' [HIn HP]]];
        (exists a' || exists a);
        rewrite PIn_rcons_or;
        split => //;
        by [left | right].
move => [a'].
rewrite PIn_rcons_or.
move => [[->| Hin]] HP.
    by left.
right.
by exists a'.
Qed.

(* A theory of indexed mapping                                                *)
(* This section is based on MetaCoq "utils/theories/MCList.v" commit ID:      *)
(* 82571676cbe51c0eb76806553e55c2b7bd2e34c8 which is licensed under MIT as    *)
(* follows:                                                                   *)
(* Copyright (c) 2014-2018 Gregory Malecha                                    *)
(* Copyright (c) 2015-2018 Abhishek Anand, Matthieu Sozeau                    *)
(* Copyright (c) 2017-2018 Simon Boulier, Nicolas Tabareau, Cyril Cohen       *)
(* Copyright (c) 2018-2020 Danil Annenkov, Yannick Forster, Théo Winterhalter *)

Section IMAP.
Variable A B: Type.
Variable f: nat -> A -> B.

Fixpoint imap_rec (l : seq A) (n : nat) : seq B :=
match l with
| [::] => [::]
| hd :: tl => f n hd :: imap_rec tl n.+1
end.

Definition imap (l : seq A) := imap_rec l 0.
End IMAP.

Section MapIndexRev.
Variable T U: Type.
Variable f: nat -> T -> U.
Definition rimap (s: seq T) :=
    imap (fun n => f (size s - n.+1)) s.
End MapIndexRev.

Section IMAP1.
Variable A B C: Type.
Variable f g: nat -> A -> B.
Variable h: nat -> B -> C.

Lemma imap_rec_id T (l: seq T) n:
    imap_rec (fun _ => id) l n = l.
Proof.
elim : l n => [//|a l IHl] n /=.
by rewrite IHl.
Qed.

Lemma imap_id T (l: seq T):
    imap (fun _ => id) l = l.
Proof.
by rewrite /imap imap_rec_id.
Qed.

Lemma imap_rec_ext_size l k :
    (forall k' x, PIn x l -> k' < k + size l -> f k' x = g k' x) ->
    imap_rec f l k = imap_rec g l k.
Proof.
move => Hext.
have: k <= k.
    by lia.
generalize k at 1 3 4.
elim: l k Hext => [//|a l IHl] k Hext /=.
move => k' Hle.
rewrite Hext /=;
    last first.
    - by lia.
    -   by apply pin_here.
rewrite (IHl k.+1) //.
move => k'' x Hin Hlt.
apply:Hext => /=.
    by apply: pin_future.
by lia.
Qed.

Lemma imap_ext_size l :
    (forall k x, PIn x l -> k < size l -> f k x = g k x) ->
    imap f l = imap g l.
Proof.
move => Hext.
by apply: imap_rec_ext_size.
Qed.

Lemma imap_rec_ext_size2 l k :
    (forall x l1 l2, l = l1 ++ x::l2 -> f (k + size l1) x = g (k + size l1) x) ->
    imap_rec f l k = imap_rec g l k.
Proof.
elim: l k => [//|a l IHl] k Hext /=.
f_equal.
    have := Hext a [::] l => /=.
    rewrite addn0 => Heq.
    by apply: Heq.
apply: IHl => x l1 l2 Heq.
have := Hext x (a::l1) l2 => /=.
rewrite -Heq addSnnS => Hext'.
by apply: Hext'.
Qed.

Lemma imap_ext_size2 l:
    (forall x l1 l2, l = l1 ++ x::l2 -> f (size l1) x = g (size l1) x) ->
    imap f l = imap g l.
Proof.
move => Hext.
by rewrite /imap imap_rec_ext_size2.
Qed.

Lemma imap_rec_compose k l :
    imap_rec h (imap_rec f l k) k = imap_rec (fun k x => h k (f k x)) l k.
Proof.
elim: l k => [//|a l IHl] k/=.
by rewrite IHl.
Qed.

Lemma imap_compose l : imap h (imap f l) = imap (fun k x => h k (f k x)) l.
Proof.
by apply imap_rec_compose.
Qed.

Lemma imap_rec_eqn l a n :
    imap_rec f (a :: l) n = f n a :: imap_rec f l (S n).
Proof.
by [].
Qed.

Lemma imap_map (l : seq A) (f' : A -> B) :
    imap h (map f' l) = imap (fun i x => h i (f' x)) l.
Proof.
rewrite /imap.
move: 0.
elim :l => [//|a l IHl] n /=.
by rewrite IHl.
Qed.

Lemma map_imap (l : seq A) (g' : B -> C) :
    map g' (imap f l) = imap (fun i x => g' (f i x)) l.
Proof.
rewrite /imap.
move : 0.
elim :l => [//|a l IHl] n /=.
by rewrite IHl.
Qed.

Lemma imap_imap  l :
  imap h (imap f l) = imap (fun n x => h n (f n x)) l.
Proof.
rewrite /imap.
move: 0.
elim :l => [//|a l IHl] n /=.
by rewrite IHl.
Qed.

Lemma imap_cst_map (f' : A -> B) l :
imap (fun _ => f') l = map f' l.
Proof.
rewrite /imap.
move: 0.
elim: l => [//|a l IHl] n /=.
by rewrite IHl.
Qed.

Lemma imap_rec_ext (l : seq A) n :
  (forall k x, n <= k -> k < size l + n -> f k x = g k x) ->
  imap_rec f l n = imap_rec g l n.
Proof.
elim: l n => [//|a l IHl] n Hext /=.
rewrite IHl.
    rewrite Hext //=.
    by lia.
move => ????.
apply: Hext => /=;
    by lia.
Qed.

Lemma imap_ext l : (forall n x, f n x = g n x) -> imap f l = imap g l.
Proof.
move => ?.
by apply: imap_rec_ext.
Qed.

Lemma imap_rec_Sk l k : imap_rec f l (S k) = imap_rec (fun n x => f (S n) x) l k.
Proof.
elim: l k => [//|a l IHl] k /=.
by rewrite IHl.
Qed.
End IMAP1.

Section IMAP2.
Variable A B C: Type.
Variable f g: nat -> A -> B.
Variable h: nat -> B -> C.

Lemma imap_rec_add l n k:
    imap_rec f l (n + k) = imap_rec (fun (k : nat) (x : A) => f (n + k) x) l k.
Proof.
elim: l n k => [//|a l IHl n k] /=.
have : (n + k).+1 = n.+1 + k.
    by lia.
move ->.
rewrite IHl imap_rec_Sk.
erewrite imap_rec_ext => // ???? /=.
f_equal.
by lia.
Qed.

Lemma imap_rec_app (l l' : seq A) n :
  (imap_rec f (l ++ l') n = imap_rec f l n ++ imap_rec f l' (size l + n)).
Proof.
elim: l n=> [//| a l IHl] n /=.
rewrite IHl /=.
f_equal.
f_equal.
f_equal.
by lia.
Qed.

Lemma imap_rec_n n m l:
    imap_rec f l (m + n) =
    imap_rec (fun n0 : nat => [eta f (m + n0)]) l n.
Proof.
elim: l m n => [//|a l IHl] m n /=.
have : (m + n).+1 = m + n.+1.
    by lia.
move => ->.
by rewrite IHl.
Qed.

Lemma imap_app (l l' : seq A) :
    (imap f (l ++ l') =
    imap f l ++ imap (fun n x => f (size l + n) x) l').
Proof.
rewrite /imap.
by rewrite imap_rec_app imap_rec_n.
Qed.
End IMAP2.


Section IMAP3.
Variable A B C: Type.
Variable f g: nat -> A -> B.
Variable h: nat -> B -> C.

Lemma rev_imap_rec (l : seq A) n k:
    k <= n ->
    rev (imap_rec f l (n - k)) =
    imap_rec (fun k x => f ((size l).-1 + n - k) x) (rev l) k.
Proof.
rewrite /imap.
elim/last_ind : l n k => [//|l x IHl] n k Hlt /=.
rewrite rev_rcons.
rewrite rcons_to_cat imap_rec_app.
rewrite rev_cat IHl //=.
rewrite size_cat addn1 /=.
f_equal.
    f_equal.
    by lia.
rewrite imap_rec_Sk.
apply: imap_rec_ext.
rewrite size_rev => ????.
f_equal.
by lia.
Qed.

Lemma rev_imap (l : seq A) :
  rev (imap f l) = imap (fun k x => f ((size l).-1 - k) x) (rev l).
Proof.
rewrite /imap.
change 0 with (0 - 0) at 1.
by rewrite rev_imap_rec // addn0.
Qed.

Lemma imap_rec_rev (l : seq A) n :
  imap_rec f (rev l) n = rev (imap (fun k x => f (size l + n - S k) x) l).
Proof.
rewrite /imap.
elim/last_ind: l n => [//|a l IHl] n /=.
rewrite rev_rcons /= IHl.
rewrite rcons_to_cat imap_rec_app /=.
rewrite rev_cat /=.
rewrite size_cat /= addn1 addn0.
have : (size a).+1 + n - (size a).+1 = n.
    by lia.
move => ->.
erewrite imap_rec_ext => //.
move => ???? /=.
f_equal.
by lia.
Qed.

Lemma imap_rev (l : seq A) :
  imap f (rev l) = rev (imap (fun k x => f (size l - S k) x) l).
Proof.
by rewrite /imap imap_rec_rev addn0.
Qed.

Lemma imap_rec_size (l : seq A) n : size (imap_rec f l n) = size l.
Proof.
elim: l n => [//| a l IHl] n /=.
by rewrite IHl.
Qed.

Lemma imap_size (l : seq A) : size (imap f l) = size l.
Proof.
by apply: imap_rec_size.
Qed.

Lemma imap_cons a l : imap f (a :: l) = f 0 a :: imap (fun x => f (S x)) l.
Proof.
by rewrite /imap /= imap_rec_Sk.
Qed.

Lemma imap_nth (l : seq A) (l' : seq B) (default : A) : size l = size l' ->
    imap (fun i _ => nth default l i ) l' = l.
Proof.
rewrite /imap.
elim: l' l => [//|a' l' IHl'] [|a l] //= [Heq].
by rewrite imap_rec_Sk IHl'.
Qed.

Lemma pin_imap_rec1 (l: seq A) b n:
    PIn b (imap_rec f l n) ->
    exists a l1 l2, l = l1 ++ a :: l2 /\ b = f (size l1 + n) a.
Proof.
move Heq :(imap_rec f l n) => l' Hin.
elim: Hin l n Heq => {l'} [a0 l'|a0 a1 l' Hin IH] [//|a2 l] n /= [].
    move <- => Heql'.
    by exists a2, [::], l => /=.
move => Heqa' Heql'.
have := IH _ _ Heql'.
move => [a3] [l1] [l2] [-> ->].
exists a3, (a2::l1), l2.
split => //=.
f_equal.
by lia.
Qed.

Lemma pin_imap_rec2 (l: seq A) b n:
    (exists a l1 l2, l = l1 ++ a :: l2 /\ b = f (size l1 + n) a) ->
    PIn b (imap_rec f l n).
Proof.
move => [a] [l1] [l2] [-> ->].
rewrite imap_rec_app PIn_app /=.
right.
by apply: pin_here.
Qed.

Lemma pin_imap_rec (l: seq A) b n:
    PIn b (imap_rec f l n) <->
    exists a l1 l2, l = l1 ++ a :: l2 /\ b = f (size l1 + n) a.
Proof.
split.
    by apply: pin_imap_rec1.
by apply: pin_imap_rec2.
Qed.

Lemma pin_imap (l: seq A) b:
    PIn b (imap f l) <->
    exists a l1 l2, l = l1 ++ a :: l2 /\ b = f (size l1) a.
Proof.
rewrite /imap pin_imap_rec.
split;
    move => [a] [l1] [l2] [-> ->];
    exists a, l1, l2;
    by rewrite addn0.
Qed.
End IMAP3.

Lemma imap_rec_zip {A B C D} (s1: seq A) (s2: seq B) (f: nat -> A -> C) (g: nat -> B -> D) n:
    zip (imap_rec f s1 n) (imap_rec g s2 n) = imap_rec (fun i xy => ((f i (fst xy)), (g i (snd xy)))) (zip s1 s2) n.
Proof.
elim: s2 s1 n => [|b s2 IHs2];
    elim => [|a s1 IHs1] n //=.
by rewrite IHs2.
Qed.

Lemma imap_zip {A B C D} (s1: seq A) (s2: seq B) (f: nat -> A -> C) (g: nat -> B -> D):
    zip (imap f s1) (imap g s2) = imap (fun i xy => ((f i (fst xy)), (g i (snd xy)))) (zip s1 s2).
Proof.
by rewrite /imap imap_rec_zip.
Qed.

Lemma imap_rec_cat_id T f (l l': seq T) n:
    imap_rec f (l ++ l') n = l ++ l' ->
    imap_rec f l n = l /\ imap_rec f l' (size l + n) = l'.
Proof.
elim: l l' n => [|t l IHl] l' n//=.
move => [-> /IHl [-> Heq]].
split => //.
rewrite -[in RHS]Heq.
f_equal.
by lia.
Qed.

Lemma imap_cat_id T f (l l': seq T):
    imap f (l ++ l') = l ++ l' ->
    imap f l = l /\ imap (fun n x => f (size l + n) x) l' = l'.
Proof.
rewrite /imap.
move/imap_rec_cat_id.
by rewrite imap_rec_n.
Qed.

Section RIMAP.
Variable A B C: Type.
Variable f g: nat -> A -> B.
Variable h: nat -> B -> C.

Lemma rimap_id T (l: seq T):
    rimap (fun _ => id) l = l.
Proof.
by rewrite /rimap imap_id.
Qed.

Lemma rimap_ext_size l :
    (forall k x, PIn x l -> k < size l -> f k x = g k x) ->
    rimap f l = rimap g l.
Proof.
rewrite /rimap.
move => Hext.
apply: imap_ext_size => k x Hin Hlt.
apply: Hext => //.
by lia.
Qed.

Lemma rimap_ext_size2 l:
    (forall x l1 l2, l = l1 ++ x::l2 -> f (size l2) x = g (size l2) x) ->
    rimap f l = rimap g l.
Proof.
move => Hext.
rewrite /imap.
apply: imap_rec_ext_size2.
move => x l1 l2 Heq.
rewrite Heq size_cat /= add0n.
replace (size l1 + (size l2).+1 - (size l1).+1) with (size l2) by lia.
apply: Hext.
apply: Heq.
Qed.

Lemma rimap_compose l : rimap h (rimap f l) = rimap (fun k x => h k (f k x)) l.
Proof.
rewrite /rimap.
by rewrite imap_compose imap_size.
Qed.

Lemma rimap_map (l : seq A) (f' : A -> B) :
    rimap h (map f' l) = rimap (fun i x => h i (f' x)) l.
Proof.
by rewrite /rimap imap_map size_map.
Qed.

Lemma map_rimap (l : seq A) (g' : B -> C) :
    map g' (rimap f l) = rimap (fun i x => g' (f i x)) l.
Proof.
by rewrite /rimap map_imap.
Qed.

Lemma rimap_rimap  l :
  rimap h (rimap f l) = rimap (fun n x => h n (f n x)) l.
Proof.
by rewrite /rimap imap_imap imap_size.
Qed.

Lemma rimap_cst_map (f' : A -> B) l :
rimap (fun _ => f') l = map f' l.
Proof.
by rewrite /rimap imap_cst_map.
Qed.

Lemma rimap_ext l : (forall n x, f n x = g n x) -> rimap f l = rimap g l.
Proof.
move => ?.
by apply: imap_ext.
Qed.

Lemma rimap_app (l l' : seq A) :
    (rimap f (l ++ l') =
    rimap (fun n x => f (size l' + n) x) l ++ rimap f l').
Proof.
rewrite /rimap imap_app.
rewrite size_cat.
f_equal;
    eapply imap_rec_ext => k x _;
    rewrite addn0 => Hlt;
    f_equal;
    by lia.
Qed.

Lemma rev_rimap_imap (l : seq A) :
  rev (rimap f l) = imap f (rev l).
Proof.
rewrite /rimap rev_imap.
apply: imap_ext_size => k x Hin.
rewrite size_rev => Hlt.
f_equal.
by lia.
Qed.

Lemma rimap_size (l : seq A) : size (rimap f l) = size l.
Proof.
by rewrite /rimap imap_size.
Qed.

Lemma rimap_cons a l : rimap f (a :: l) = f (size l) a :: rimap f l.
Proof.
rewrite /rimap.
rewrite imap_cons /=.
repeat f_equal.
by lia.
Qed.

Lemma pin_rimap (l: seq A) b:
    PIn b (rimap f l) <->
    exists a l1 l2, l = l1 ++ a :: l2 /\ b = f (size l2) a.
Proof.
rewrite /rimap pin_imap.
split;
    move => [a] [l1] [l2] [-> ->];
    exists a, l1, l2;
    rewrite size_cat /=;
    split => //;
    f_equal;
    by lia.
Qed.
End RIMAP.

Lemma rimap_cat_id T f (l l': seq T):
    rimap f (l ++ l') = l ++ l' ->
    rimap (fun n x => f (size l' + n) x) l = l /\ rimap f l' = l'.
Proof.
Proof.
rewrite /rimap size_cat.
move /imap_cat_id => [Heql Heql'].
split.
    rewrite -[in RHS]Heql.
    apply: imap_ext_size => k x Hin Hlt.
    f_equal.
    by lia.
rewrite -[in RHS]Heql'.
apply: imap_ext_size => k x Hin Hlt.
f_equal.
by lia.
Qed.

Lemma rimap_zip {A B C D} (s1: seq A) (s2: seq B) (f: nat -> A -> C) (g: nat -> B -> D):
    size s1 = size s2 ->
    zip (rimap f s1) (rimap g s2) = rimap (fun i xy => ((f i (fst xy)), (g i (snd xy)))) (zip s1 s2).
Proof.
move => Heq.
rewrite /rimap imap_zip.
rewrite size_zip Heq.
by rewrite minnn.
Qed.

(* This section is based on:                                                  *)
(*   https://github.com/imdea-software/fcsl-pcm/blob/master/core/seqperm.v    *)
(* commit id: 79bb8b3eae4d6c682a757b0c26f282ce378dab52                        *)

(****************************************************)
(* A theory of permutations over non-equality types *)
(****************************************************)

Reserved Infix "≡ₚ" (at level 70, no associativity).
Inductive perm {A} : seq A -> seq A -> Prop :=
| permutation_nil : [::] ≡ₚ [::]
| permutation_skip x s1 s2: s1 ≡ₚ s2 -> (x :: s1) ≡ₚ (x :: s2)
| permutation_swap x y s1 s2: s1 ≡ₚ s2 -> [:: x, y & s1] ≡ₚ [:: y, x & s2]
| permutation_trans t s1 s2: s1 ≡ₚ t -> t ≡ₚ s2 -> s1 ≡ₚ s2
where "x ≡ₚ y" := (perm x y).

Section Perm.
Context {A : Type}.


Lemma perm_refl (s : seq A) : s  ≡ₚ s.
Proof.
elim: s=> [| a l IHl].
    by apply: permutation_nil.
by apply: permutation_skip.
Qed.

Lemma perm_nil (s : seq A) : [::] ≡ₚ s <-> s = [::].
Proof.
split.
    move E: {1}[::]=>l H.
    move: H {E}(esym E).
    by elim=>//??? _ IH1 _ IH2 /IH1/IH2.
move=>->.
by apply: permutation_nil.
Qed.

Lemma perm_sym (s1 s2: seq A) : s1 ≡ₚ s2 <-> s2 ≡ₚ s1.
Proof.
suff {s1 s2} L : forall s1 s2, s1 ≡ₚ s2 -> s2 ≡ₚ s1.
    split;
        by apply: L.
move => T s1 s2.
elim {s1 s2} =>[
    |x s1 s2 HP12 HP32
    |x y s1 s2 HP12 HP21
    |s1 s2 s3 HP21 HP12 HP13 HP31].
+   by apply: permutation_nil.
+   by apply: permutation_skip.
+   by apply: permutation_swap.
+   by apply: permutation_trans HP31 HP12.
Qed.

Lemma perm_trans (s2 s1 s3: seq A) : s1 ≡ₚ s2 -> s2 ≡ₚ s3 -> s1 ≡ₚ s3.
Proof.
by apply: permutation_trans.
Qed.

Lemma perm_in (s1 s2: seq A) x : s1 ≡ₚ s2 -> PIn x s1 -> PIn x s2.
Proof.
elim =>
    [|x' s3 s4 Hperm34 Hin34
     |x' y' s3 s4 Hperm34 Hin34
     | s4 s3 s5 Hperm34 Hin34 Hperm45 Hin45];
     rewrite ?PIn_cons_or.
-   by [].
-   move => [<-|Hin3].
        by left.
    right.
    by apply: Hin34.
-   move =>[<-|[<-|Hin3]].
    +   right.
        by left.
    +   by left.
    +   repeat right.
        by apply: Hin34.
-   move => Hin3.
    have Hin4 := Hin34 Hin3.
    by apply: Hin45.
Qed.

Lemma perm_catC (s1 s2: seq A) : (s1 ++ s2) ≡ₚ (s2 ++ s1).
Proof.
elim: s1 s2=>[|x s1 IH1] s2 /=.
    rewrite cats0.
    by apply: perm_refl.
apply: (@perm_trans (x::s2++s1)).
    by apply: permutation_skip.
elim: s2=>[|y s2 IH2] //=.
    by apply: perm_refl.
apply: (@perm_trans (y::x::s2++s1)).
    apply: permutation_swap.
    by apply: perm_refl.
by apply: permutation_skip.
Qed.

Lemma perm_cat2lL (s s1 s2: seq A) : s1 ≡ₚ s2 -> (s ++ s1) ≡ₚ (s ++ s2).
Proof.
elim: s=>[//|e s IH /IH];
    by apply: permutation_skip.
Qed.

Lemma perm_cat2rL (s s1 s2: seq A) : s1 ≡ₚ s2 -> (s1 ++ s) ≡ₚ (s2 ++ s).
Proof.
move=>?.
apply: (@perm_trans (s ++ s1)).
    by apply: perm_catC.
apply: (@perm_trans (s ++ s2)).
    by apply: perm_cat2lL.
by apply: perm_catC.
Qed.

Lemma perm_catL (s1 t1 s2 t2: seq A) :
        s1 ≡ₚ s2 -> t1 ≡ₚ t2 -> (s1 ++ t1) ≡ₚ (s2 ++ t2).
Proof.
move/(perm_cat2rL t1)=>H1 /(perm_cat2lL s2).
by apply: perm_trans.
Qed.

Lemma perm_cat_consL (s1 t1 s2 t2: seq A)  x :
        s1 ≡ₚ s2 -> t1 ≡ₚ t2 -> (s1 ++ x :: t1) ≡ₚ (s2 ++ x :: t2).
Proof.
move=>*.
apply: perm_catL.
    by [].
by apply: permutation_skip.
Qed.

Lemma perm_cons_catCA (s1 s2: seq A) x : (x :: s1 ++ s2) ≡ₚ (s1 ++ x :: s2).
Proof.
rewrite -cat1s -(cat1s _ s2) !catA.
by apply/perm_cat2rL/perm_catC.
Qed.

Lemma perm_cons_catAC (s1 s2: seq A) x : (s1 ++ x :: s2) ≡ₚ (x :: s1 ++ s2).
Proof.
by apply/perm_sym/perm_cons_catCA.
Qed.

Lemma perm_cons_cat_consL (s1 s2 s: seq A) x :
        s  ≡ₚ (s1 ++ s2) -> (x :: s) ≡ₚ (s1 ++ x :: s2).
Proof.
move=>?.
apply: (@perm_trans (x :: (s1 ++ s2))).
    by apply: permutation_skip.
by apply: perm_cons_catCA.
Qed.

Lemma perm_size (l1 l2: seq A): l1 ≡ₚ l2 -> size l1 = size l2.
Proof.
by elim=>//=???? =>[|?|]->.
Qed.

Lemma perm_cat_consR (s1 s2 t1 t2: seq A) x :
        (s1 ++ x :: t1) ≡ₚ (s2 ++ x :: t2) -> (s1 ++ t1) ≡ₚ (s2 ++ t2).
Proof.
move: s1 t1 s2 t2 x.
suff H:
    forall (r1 r2: seq A), r1 ≡ₚ r2 -> forall x s1 t1 s2 t2,
        r1 = s1 ++ x :: t1 -> r2 = s2 ++ x :: t2 -> (s1 ++ t1) ≡ₚ (s2 ++ t2).
    move=>s1 t1 s2 t2 x /H H'. by apply: H'.
move => r1 r2.
elim {r1 r2}=> [];
    last 1 first.
-   move=>s2 s1 s3 H1 IH1 H2 IH2 x r1 t1 r2 t2 E1 E2.
    case: (@PIn_split1 _ x s2).
    -   apply: perm_in H1 _.
        rewrite E1 PIn_app.
        right.
        left.
    -   move=>s4 [s5] E.
        apply: (@perm_trans (s4++s5)).
            by apply: IH1 E1 E.
        by apply: IH2 E E2.
-   by move=>x [].
-   move=>x t1 t2 H IH y [|b s1] s2 [|c p1] p2 /= [E1 E2] [E3 E4];
        subst x;
        move: H;
        rewrite ?E1 ?E2 ?E3 ?E4 =>// H.
    -   subst y.
        apply: perm_trans H _.
        rewrite perm_sym.
        apply: perm_cons_cat_consL.
        by apply: perm_refl.
    -   apply: perm_trans H.
        apply: perm_cons_cat_consL.
        by apply: perm_refl.
    -   apply: permutation_skip.
        by apply: IH E2 E4.
move=>x y p1 p2 H IH z [|b s1] t1 [|c s2] t2 /= [E1 E2] [E3 E4];
    subst x y;
    move : H IH;
    rewrite -?E2 -?E4 => H IH.
-   by apply: permutation_skip.
-   case: s2 E4=>/=[|a s2][<-]=>[|E4];
        apply: permutation_skip.
        by [].
    subst p2.
    apply: perm_trans H _.
    by apply: perm_cons_catAC.
-   case: s1 E2=>/=[|a s1][<-]=>[|E2];
        apply: permutation_skip.
        by [].
    subst p1.
    apply: perm_trans H.
    by apply: perm_cons_catCA.
case: s1 E2=>/=[|a s1][->]=>E2;
    case: s2 E4=>/=[|d s2][->]=>E4;
    move : H IH;
    rewrite ?E2 ?E4 => H IH.
-   by apply: permutation_skip.
-   apply: (@perm_trans [:: d, z & s2 ++ t2]);
        last first.
        apply: permutation_swap.
        by apply: perm_refl.
    apply: permutation_skip.
    apply: perm_trans H _.
    by apply/perm_cons_catAC.
-   apply: (@perm_trans [:: a, z & s1 ++ t1]).
        apply: permutation_swap.
        by apply: perm_refl.
    apply: permutation_skip.
    by apply/perm_trans/H/perm_cons_catCA.
-   apply: permutation_swap.
    by apply: IH.
Qed.

Lemma perm_cons x (s1 s2: seq A): (x :: s1) ≡ₚ (x :: s2) <-> s1 ≡ₚ s2.
Proof.
split.
   by apply/(@perm_cat_consR [::] [::]).
by apply: permutation_skip.
Qed.

Lemma perm_cat2l (s s1 s2: seq A):  (s ++ s1) ≡ₚ (s ++ s2) <-> s1 ≡ₚ s2.
Proof.
split.
    by elim: s=>// ??? /perm_cons.
by apply: perm_cat2lL.
Qed.

Lemma perm_cat2r (s s1 s2: seq A) : (s1 ++ s) ≡ₚ (s2 ++ s) <-> s1 ≡ₚ s2.
Proof.
split;
    last by apply: perm_cat2rL.
elim: s=>[|??? /perm_cat_consR].
    by rewrite !cats0.
by [].
Qed.

Lemma perm_catAC (s1 s2 s3: seq A) : ((s1 ++ s2) ++ s3) ≡ₚ ((s1 ++ s3) ++ s2).
Proof.
rewrite -!catA perm_cat2l.
by apply: perm_catC.
Qed.

Lemma perm_catCA (s1 s2 s3: seq A) : (s1 ++ s2 ++ s3) ≡ₚ (s2 ++ s1 ++ s3).
Proof.
rewrite !catA perm_cat2r.
by apply: perm_catC.
Qed.

Lemma perm_cons_cat_cons x (s1 s2 s: seq A) :
        (x :: s) ≡ₚ (s1 ++ x :: s2) <-> s  ≡ₚ (s1 ++ s2).
Proof.
split.
    by apply: (@perm_cat_consR [::]).
by apply: perm_cons_cat_consL.
Qed.

Lemma perm_cat_cons x (s1 s2 t1 t2: seq A) :
        (s1 ++ x :: t1) ≡ₚ (s2 ++ x :: t2) <-> (s1 ++ t1) ≡ₚ (s2 ++ t2).
Proof.
split=>[|H].
    by apply: perm_cat_consR.
apply: (@perm_trans (x::s1++t1)).
    by apply: perm_cons_catAC.
apply: (@perm_trans (x::s2++t2)).
    by apply: permutation_skip.
rewrite perm_sym.
apply: perm_cons_catAC.
Qed.

Lemma perm_empty_r (s: seq A) : s = [::] <-> s ≡ₚ [::].
Proof.
split.
    move ->.
    apply: perm_refl.
move Heqs' : [::] => s' HP.
rewrite -Heqs'.
elim : HP Heqs' => {s s'} [
    |x' s1 s2 HP12 IH
    |x' y s1 s2 HP12 Heq
    |s2 s1 s3 HP12 Heq12 HP23 Heq23] H //.
apply: Heq12.
symmetry.
by apply: Heq23.
Qed.

Lemma perm_empty_l (s: seq A) : [::] = s <-> [::] ≡ₚ s.
Proof.
rewrite perm_sym -perm_empty_r.
split;
    by move ->.
Qed.

Lemma perm_singleton_r x (s: seq A): s = [::x] <-> s ≡ₚ [::x].
Proof.
split.
    move ->.
    apply: perm_refl.
move Heqs' : [::x] => s' HP.
rewrite -Heqs'.
elim : HP Heqs' => {s s'} [
    |x' s1 s2 HP12 IH
    |x' y s1 s2 HP12 Heq
    |s2 s1 s3 HP12 Heq12 HP23 Heq23] //=.
-   move => [<-] Hnil.
    move: HP12.
    rewrite -Hnil -perm_empty_r.
    by move ->.
-   move => Heq3.
    apply: Heq12.
    symmetry.
    by apply: Heq23.
Qed.

Lemma perm_singleton_l x (s: seq A): [::x] = s <-> [::x] ≡ₚ s.
Proof.
rewrite perm_sym -perm_singleton_r.
split;
    by move ->.
Qed.

Lemma foldr_perm (f: A -> A -> A) b (s1 s2: seq A):
    associative f ->
    commutative f ->
    s1 ≡ₚ s2 -> foldr f b s1 = foldr f b s2.
Proof.
move => Hassoc Hcomm.
elim => {s1 s2} [
    |x' s1 s2 HP12 IH
    |x' y s1 s2 HP12 Heq
    |s2 s1 s3 HP12 Heq12 HP23 Heq23] /=.
-   by [].
-   by rewrite IH.
-   by rewrite Hassoc (@Hcomm x') -Hassoc Heq.
-   by rewrite Heq12 Heq23.
Qed.

End Perm.

(* perm and map *)
Lemma pperm_map A B (f : A -> B) (s1 s2 : seq A) :
        s1 ≡ₚ s2 -> (map f s1) ≡ₚ (map f s2).
Proof.
elim => [
    |x s3 s4 HP34 HPmap34
    |x y s3 s4 HP34 HPmap34
    |s3 s4 s5 HP34 HPmap34 Hp34 HPmap45] /=.
-   apply: perm_refl.
-   by rewrite perm_cons.
-   by apply: permutation_swap.
-   apply: perm_trans.
        apply: HPmap34.
    apply: HPmap45.
Qed.

(* mapping to ssreflect decidable perm *)
Lemma perm_eq_perm (A : eqType) (s1 s2 : seq A) :
        reflect (s1 ≡ₚ s2) (perm_eq s1 s2).
Proof.
apply: (iffP idP).
    elim: s2 s1 =>[s1 /ssreflect.seq.perm_size/size0nil->// | x s2 IH s1 H].
    -   apply: perm_refl.
    -   move: (seq.perm_mem H x).
        rewrite mem_head=>H'.
        move: H' H.
        move/splitPr=>[p1 p2].
        rewrite -cat1s ssreflect.seq.perm_catCA.
        rewrite ssreflect.seq.perm_cons=>/IH.
        by rewrite -[_::s2]cat0s perm_cat_cons.
elim=>[|||??? _ H1 _ H2] /=.
-   by [].
-   move => x s3 s4.
    by rewrite ssreflect.seq.perm_cons.
-   move => x y s3 s4.
    rewrite -![[:: _, _ & _]]/([::_] ++ [::_] ++ _) ssreflect.seq.perm_catCA.
    by rewrite !ssreflect.seq.perm_cat2l.
-   by apply: ssreflect.seq.perm_trans H1 H2.
Qed.


(* The definition and lemmas for submseteq are taken straight from stdpp. I   *)
(* guess I am too dump to come up with that myself :\                         *)

(* A seq [l2] submseteq a seq [l1] if [l2] is obtained by removing elements *)
(* from [l1] while possiblity changing the order. *)
Inductive submseteq {A} : seq A -> seq A -> Prop :=
  | submseteq_nil : submseteq [::] [::]
  | submseteq_skip x l1 l2 : submseteq l1 l2 -> submseteq (x :: l1) (x :: l2)
  | submseteq_swap x y l : submseteq (y :: x :: l) (x :: y :: l)
  | submseteq_cons x l1 l2 : submseteq l1 l2 -> submseteq l1 (x :: l2)
  | submseteq_trans l1 l2 l3 : submseteq l1 l2 -> submseteq l2 l3 -> submseteq l1 l3.
Infix "⊆+" := submseteq (at level 70).

Lemma submseteq_size A (l1 l2: seq A) : l1 ⊆+ l2 -> size l1 <= size l2.
Proof.
elim => /=;
    by lia.
Qed.

Lemma submseteq_nil_l A (l: seq A) : [::] ⊆+ l.
Proof.
elim : l => [|a l IHl].
    by constructor.
by constructor.
Qed.

Lemma submseteq_nil_r A (l: seq A) : l ⊆+ [::] <-> l = [::].
Proof.
split;
    last first.
    move ->.
    by constructor.
move /submseteq_size.
case : l => [|a l] /=.
    by [].
by lia.
Qed.

Lemma Permutation_submseteq A (l1 l2: seq A) : l1 ≡ₚ l2 -> l1 ⊆+ l2.
Proof.
elim => {l1 l2} => [
    |x s1 s2 HP12 HS12
    |x y s1 s2 HP12 HS12
    |s2 s1 s3 HP12 HS12 HP23 HS23].
-   by constructor.
-   by constructor.
-   apply: submseteq_trans.
        apply: submseteq_swap.
    by repeat apply: submseteq_skip.
-   apply: submseteq_trans.
    by apply: HS12.
    by apply: HS23.
Qed.

Lemma submseteq_Permutation A (l1 l2: seq A) : l1 ⊆+ l2 -> exists k, l2 ≡ₚ l1 ++ k.
Proof.
elim => {l1 l2} [
    |a l1 l2 HS12 [k HP12k]
    |a b l1
    |a l1 l2 HP12 [k HP12k]
    |l1 l2 l3 HP12 [k HP21k] HP23 [k' HP32k']].
-   exists [::] => /=.
    apply: perm_refl.
-   exists k.
    rewrite cat_cons.
    by apply: permutation_skip.
-   exists [::].
    rewrite cats0.
    apply: permutation_swap.
    apply: perm_refl.
-   exists (a :: k).
    by rewrite perm_cons_cat_cons.
-   exists (k ++ k').
    apply: permutation_trans.
        apply: HP32k'.
    by rewrite catA perm_cat2r.
Qed.
Lemma seq_app_size A (l1 l2: seq A):
    size (l1 ++ l2) = size l1 + size l2.
Proof.
elim : l1 l2 => [|a l IHl] l2 /=.
    by lia.
rewrite IHl.
by lia.
Qed.

Lemma submseteq_Permutation_size_le A (l1 l2: seq A) :
    size l2 <= size l1 -> l1 ⊆+ l2 -> l1 ≡ₚ l2.
Proof.
move => Hl12 HS12.
move : (submseteq_Permutation HS12) =>[[|a s3]].
    by rewrite cats0 perm_sym.
rewrite perm_sym.
move => /Permutation_submseteq/submseteq_size.
rewrite seq_app_size /=.
by lia.
Qed.

Lemma submseteq_Permutation_size_eq A (l1 l2: seq A) :
  size l2 = size l1 -> l1 ⊆+ l2 -> l1 ≡ₚ l2.
Proof.
move => Hl12.
apply submseteq_Permutation_size_le.
by lia.
Qed.

Lemma submseteq_Permutation_alt A (l1 l2: seq A):
    l1 ⊆+ l2 -> l2 ⊆+ l1 -> l1 ≡ₚ l2.
move => HS12 HS21.
apply: submseteq_Permutation_size_eq;
    last by [].
move: HS12 HS21.
move /submseteq_size => Hl12 /submseteq_size => Hl21.
by lia.
Qed.

Lemma submseteq_inserts_l A (l1 l2 l3: seq A):
    l1 ⊆+ l2 -> l1 ⊆+ l3 ++ l2.
Proof.
elim : l3 l1 l2 => [|a l3 IHl] l1 l2 HS12 /=.
    by [].
constructor.
by apply: IHl.
Qed.

Lemma Puniq_submseteq A (l k: seq A) :
    PUniq l -> (forall x, PIn x l -> PIn x k) -> l ⊆+ k.
Proof.
move => Huniq.
elim : Huniq k => {l} [| a l Hnotinl Huniql IHl] k Hinin.
    by apply: submseteq_nil_l.
have Hinak: PIn a k.
    apply: Hinin.
    by apply: pin_here.
move :(@PIn_split1 _ a k Hinak) => [s1 [s2 Hk]].
subst.
apply: (@submseteq_trans _ _ (a:: s1 ++ s2));
    last first.
    apply: Permutation_submseteq.
    apply: perm_cons_catCA.
constructor.
apply: IHl => x Hin.
have Hororor: PIn x s1 \/ x = a \/ PIn x s2.
    rewrite -PIn_cons_or -PIn_app.
    apply: Hinin.
    by right.
rewrite PIn_app.
move : Hororor Hin.
move => [Hin1|[->|Hin2]] Hinl.
-   by left.
-   by [].
-   by right.
Qed.

Lemma Puniq_Permutation A (l1 l2: seq A) :
    PUniq l1 -> PUniq l2 -> (forall x, PIn x l1 <-> PIn x l2) -> l1 ≡ₚ l2.
Proof.
move => Huniq1 Huniq2 Hinin.
apply: submseteq_Permutation_alt;
    apply: Puniq_submseteq => //;
    move => x;
    by rewrite Hinin.
Qed.


(*nth element with none *)
Fixpoint nth_error A (l:list A) (n:nat) : option A :=
match n, l with
| O, a :: _ => Some a
| S n', _ :: l => nth_error l n'
| _, _ => None
end.

Lemma nth_error_map_some A B (s: seq A) a i (f: A-> B):
        nth_error s i = Some a ->
        nth_error (map f s) i = Some (f a).
Proof.
elim: s i => [|a' s IHs] [|i]//=.
    by move => [->].
by apply: IHs.
Qed.

Lemma nth_error_map_none A B (s: seq A) i (f: A-> B):
    nth_error s i = None ->
    nth_error (map f s) i = None.
Proof.
elim: s i => [|a' s IHs] [|i]//=.
by apply: IHs.
Qed.

Lemma nth_error_map_some_ex A B (s: seq A) a i (f: A-> B):
    nth_error (map f s) i = Some a ->
    exists b,
    nth_error s i = Some b /\ a = f b.
Proof.
elim: s i=> [|e s IHs] [|i] //=.
    move => [?].
    by exists e.
by apply: IHs.
Qed.


Lemma nth_error_size_some {A B} (a: A) la (lb: seq B) idx:
    size la = size lb ->
    nth_error la idx = Some a ->
    exists b, nth_error lb idx = Some b.
Proof.
elim: la lb idx => [|a' la IHla] [|b' lb] [|idx] //= [Hsize].
    move => _.
    by exists b'.
by apply: IHla.
Qed.

Lemma nth_error_size_none {A B} (la: seq A) (lb: seq B) idx:
    size la = size lb ->
    nth_error la idx = None ->
    nth_error lb idx = None.
Proof.
elim: la lb idx => [|a' la IHla] /= [|b' lb] [|idx] //= [Hsize].
by apply: IHla.
Qed.

Lemma nth_error_app1 A (l l': seq A) n : n < size l ->
    nth_error (l++l') n = nth_error l n.
Proof.
elim: l l' n => [|a l IHl] l' [|n]//= Hlt.
by apply: IHl.
Qed.

Lemma nth_error_app2 A (l l': seq A) n : n >= size l ->
    nth_error (l++l') n = nth_error l' (n - size l).
Proof.
elim: l l' n => [|a l IHl] l' [|n] //= Hsize.
replace (n.+1 - (size l).+1) with (n - (size l)) by lia.
by apply: IHl.
Qed.

Lemma pin_nth_error_some1 A (a: A) s:
    PIn a s -> exists idx, nth_error s idx = Some a.
Proof.
elim => {a s}[a s|a b s Hin].
    by exists 0.
move => [idx Hnth_error].
by exists idx.+1.
Qed.

Lemma pin_nth_error_some2 A (a: A) s idx:
    nth_error s idx = Some a -> PIn a s.
Proof.
elim: s a idx => [|a' s IHs] a [|idx] //=.
    move => [->].
    by apply: pin_here.
move => Hnth_error.
apply: pin_future.
apply: IHs.
by apply: Hnth_error.
Qed.

Lemma pin_nth_error_some A (a: A) s:
    PIn a s <-> exists idx, nth_error s idx = Some a.
Proof.
split.
    by apply: pin_nth_error_some1.
move => [].
by apply: pin_nth_error_some2.
Qed.

Lemma zip_nth_error_some1 {A B} (la: seq A) (lb: seq B) idx a b:
    (nth_error la idx = Some a /\ nth_error lb idx = Some b) ->
    nth_error (zip la lb) idx = Some (a, b).
Proof.
move => [].
elim: la lb idx => [|a' la IHla] [|b' lb] [|idx] //=.
    by move => [->] [->].
by apply: IHla.
Qed.

Lemma zip_nth_error_some2 {A B} (la: seq A) (lb: seq B) idx a b:
    nth_error (zip la lb) idx = Some (a, b) ->
    (nth_error la idx = Some a /\ nth_error lb idx = Some b).
Proof.
elim: la lb idx => [|a' la IHla] [|b' lb] [|idx] //=.
    by move => [-> ->].
by move /IHla.
Qed.

Lemma zip_nth_error_some {A B} (la: seq A) (lb: seq B) idx a b:
    (nth_error la idx = Some a /\ nth_error lb idx = Some b) <->
    nth_error (zip la lb) idx = Some (a, b).
Proof.
split.
    by apply: zip_nth_error_some1.
by apply: zip_nth_error_some2.
Qed.

(* l and l' are identical except for one element that satisfies R *)
Definition on_one A (R: A -> A -> Prop) l l' :=
    exists l0 l1 x y, l = l0 ++ x :: l1 /\ l' = l0 ++ y :: l1 /\ R x y.

Lemma on_one_cons A R l l' (a b: A) :
    on_one R (a::l) (b::l') <->
    (R a b /\ l = l') \/ (a = b /\ on_one R l l').
Proof.
split.
    move => [[|c l1]] [l2] [x] [y] /= [[-> ->]] [[-> ->]].
        by left.
    right.
    split => //.
    by exists l1, l2, x ,y.
move => [[HR ->]|[-> ]].
    by exists [::], l', a, b.
move => [l1] [l2] [x] [y] [->] [->] HR.
by exists (b::l1), l2, x, y.
Qed.

Lemma on_one_singleton A (R: A -> A -> Prop) x y : R x y -> @on_one A R [:: x] [:: y].
Proof.
move => HR.
by exists [::], [::], x ,y.
Qed.


Lemma on_one_app A (R : A -> A-> Prop) l l' l1 l2:
    on_one R l l' -> on_one R (l1 ++ l ++ l2) (l1 ++ l' ++ l2).
move => [l3] [l4] [x] [y] [->] [->] HR /=.
exists (l1 ++ l3), (l4 ++ l2), x, y.
by rewrite -!catA.
Qed.

Definition seq_forall_pair A B (R: A -> B -> Prop) s1 s2 :=
    size s1 = size s2 /\ forall ts, PIn ts (zip s1 s2) -> R (ts.1) (ts.2).


Lemma seq_forall_pair_cons A1 A2 (a1: A1) (a2: A2) s1 s2 (R: A1 -> A2 -> Prop):
        seq_forall_pair R (a1::s1) (a2::s2) <->
        R a1 a2 /\ seq_forall_pair R s1 s2.
Proof.
split => /=.
    move => [[Hsize]] Hforall.
    repeat split => //.
        have := Hforall (a1, a2) => /= HRa12.
        apply: HRa12.
        by apply: pin_here.
    move => ts Hin.
    apply: Hforall => /=.
    by apply: pin_future.
rewrite /seq_forall_pair /=.
move => [HR [-> Hforall]].
split => //.
move => [a1' a2'] /=.
rewrite PIn_cons_or =>  [[[-> ->]|]] // Hin.
by have := Hforall _ Hin => /=.
Qed.

Lemma seq_forall_pair_empty
    A B (R: A -> B -> Prop):
    seq_forall_pair R [::] [::].
Proof.
split => // ts.
by rewrite PIn_empty_false_iff.
Qed.

Lemma seq_forall_pair_refl
    A1 s (R: A1 -> A1 -> Prop):
    (forall a, R a a) ->
    seq_forall_pair R s s.
Proof.
move => Hrefl.
elim: s=> [|a s IHs];
    last by rewrite seq_forall_pair_cons.
split => //.
move => /= ts.
by rewrite PIn_empty_false_iff.
Qed.

Lemma seq_pair_forall_empty_consr A B (R : A -> B -> Prop ) a s:
    seq_forall_pair R [::] (a::s) <-> False.
Proof.
split => //.
by move => [].
Qed.

Lemma seq_pair_forall_empty_consl A B (R : A -> B -> Prop ) a s:
    seq_forall_pair R (a::s) [::] <-> False.
Proof.
split => //.
by move => [].
Qed.

Lemma seq_pair_forall_emptyl A B (R : A -> B -> Prop ) s:
    seq_forall_pair R [::] s <-> s = [::].
Proof.
elim: s => [|a s IH].
    split => // _.
    by apply: seq_forall_pair_empty.
split => //.
by rewrite seq_pair_forall_empty_consr.
Qed.

Lemma seq_pair_forall_emptyr A B (R : A -> B -> Prop ) s:
    seq_forall_pair R s [::] <-> s = [::].
Proof.
elim: s => [|a s IH].
    split => // _.
    by apply: seq_forall_pair_empty.
split => //.
by rewrite seq_pair_forall_empty_consl.
Qed.

Lemma seq_pair_forall_pair_singleton A B a1 a2 (R : A -> B -> Prop):
    seq_forall_pair R [:: a1] [:: a2] <->
    R a1 a2.
Proof.
rewrite /seq_forall_pair /=.
split.
    move => [_ HR].
    have := (HR (a1, a2)) => /= HR'.
    apply: HR'.
    by rewrite -PIn_singlton.
move => HR.
split => //.
move => [??].
by rewrite -PIn_singlton => [[-> ->]].
Qed.

Lemma seq_forall_pair_app A B s1 s2 s3 s4 (R : A -> B -> Prop ):
    seq_forall_pair R s1 s3 ->
    seq_forall_pair R s2 s4 ->
    seq_forall_pair R (s1++s2) (s3++s4).
Proof.
elim: s1 s3 s2 s4 => [|a1 s1 IHs1] [|a3 s3] s2 s4 //;
    rewrite ?seq_pair_forall_emptyl ?seq_pair_forall_emptyr //=.
rewrite !seq_forall_pair_cons.
move => [HR13] Hforall13 Hforall24.
split => //.
by apply: IHs1.
Qed.

Lemma seq_forall_pair_rcons1 A1 A2 (a1: A1) (a2: A2) s1 s2 (R: A1 -> A2 -> Prop):
seq_forall_pair R (rcons s1 a1) (rcons s2 a2) ->
R a1 a2 /\ seq_forall_pair R s1 s2.
Proof.
rewrite /seq_forall_pair !size_rcons => [[[Hsize]]].
move => Hforall.
repeat split => //.
    have := Hforall (a1, a2) => /= Hforall12.
    apply: Hforall12.
    rewrite zip_rcons // PIn_rcons_or.
    by left.
move => ts Hin.
apply: Hforall.
rewrite zip_rcons // PIn_rcons_or.
by right.
Qed.

Lemma seq_forall_pair_rcons2 A1 A2 (a1: A1) (a2: A2) s1 s2 (R: A1 -> A2 -> Prop):
    R a1 a2 -> seq_forall_pair R s1 s2 ->
    seq_forall_pair R (rcons s1 a1) (rcons s2 a2).
Proof.
move => HR [Hsize Hforall].
split.
    by rewrite !size_rcons Hsize.
move => ts.
rewrite zip_rcons // PIn_rcons_or => [[->|Hin]] //.
by apply: Hforall.
Qed.

Lemma seq_forall_pair_rcons A1 A2 (a1: A1) (a2: A2) s1 s2 (R: A1 -> A2 -> Prop):
seq_forall_pair R (rcons s1 a1) (rcons s2 a2) <->
R a1 a2 /\ seq_forall_pair R s1 s2.
Proof.
split.
    by apply: seq_forall_pair_rcons1.
move => [??].
by apply: seq_forall_pair_rcons2.
Qed.

Lemma seq_forall_pair_rconsl_ex A1 A2 (a1: A1) s1 s2 (R: A1 -> A2 -> Prop):
    seq_forall_pair R (rcons s1 a1) s2 ->
    exists a2 s3,
    s2 = rcons s3 a2 /\
    R a1 a2 /\ seq_forall_pair R s1 s3.
Proof.
elim/last_ind: s2 s1 a1 => [|s2 a2 IH] s1 a1.
    rewrite seq_pair_forall_emptyr rcons_to_cat.
    by elim: s1.
rewrite seq_forall_pair_rcons => [[HR Hforall]].
by exists a2, s2.
Qed.

Lemma seq_forall_pair_rconsr_ex A1 A2 (a2: A2) s1 s2 (R: A1 -> A2 -> Prop):
    seq_forall_pair R s1 (rcons s2 a2) ->
    exists a1 s3,
    s1 = rcons s3 a1 /\
    R a1 a2 /\ seq_forall_pair R s3 s2.
Proof.
elim/last_ind: s1 s2 a2 => [|s1 a1 IH] s2 a2.
    rewrite seq_pair_forall_emptyl rcons_to_cat.
    by elim: s2.
rewrite seq_forall_pair_rcons => [[HR Hforall]].
by exists a1, s1.
Qed.


Lemma seq_forall_pair_in A1 A2 (a1: A1) (a2: A2) s1 s2 idx (R: A1 -> A2 -> Prop):
    seq_forall_pair R s1 s2 ->
    nth_error s1 idx = Some a1 ->
    nth_error s2 idx = Some a2 ->
    R a1 a2.
Proof.
move => [Hsize] Hforall Hin1 Hin2.
have := Hforall (a1, a2) => /= Hforall'.
apply: Hforall'.
rewrite pin_nth_error_some.
exists idx.
by rewrite -zip_nth_error_some.
Qed.

Lemma seq_forall_pair_map A B C D (s1 :seq C) (s2 :seq D) f g (R : A -> B -> Prop):
    seq_forall_pair R (map f s1) (map g s2) <->
    seq_forall_pair (fun a b => R (f a) (g b)) s1 s2.
Proof.
split.
    move => [].
    rewrite !size_map => Hsize Hforall.
    split => //.
    move => [t1 t2] Hin/=.
    have := Hforall (f t1, g t2) => /= Hforall'.
    apply: Hforall'.
    rewrite map_zip2 pin_map.
    by exists (t1, t2).
move => [Hsize] Hforall.
split.
    by rewrite !size_map.
move => [a b].
rewrite map_zip2 pin_map.
move => [ts] [[-> ->]].
by apply: Hforall.
Qed.

Lemma seq_pair_forall_left_map A B C (s1 :seq C) s2 f (R : A -> B -> Prop):
    seq_forall_pair R (map f s1) s2 <->
    seq_forall_pair (fun a b => R (f a) b) s1 s2.
Proof.
rewrite -(map_id s2).
by rewrite seq_forall_pair_map map_id.
Qed.

Lemma seq_pair_forall_right_map A B D s1 (s2 :seq D) g (R : A -> B -> Prop):
    seq_forall_pair R s1 (map g s2) <->
    seq_forall_pair (fun a b => R a (g b)) s1 s2.
Proof.
rewrite -(map_id s1).
by rewrite seq_forall_pair_map map_id.
Qed.

Lemma seq_pair_forall_flip A B s1 s2 (R : A -> B -> Prop):
    seq_forall_pair R s1 s2 <->
    seq_forall_pair (fun x y => R y x) s2 s1.
Proof.
split;
move => [Hsize] Hforall;
split => //;
move => [b a];
rewrite Pin_zip_flip_iff;
by move /Hforall.
Qed.

Lemma seq_forall_pair_app_existsr A B (R : A -> B -> Prop) s1 s2 s3:
    seq_forall_pair R (s1++s2) s3 ->
    exists s4 s5,
        s3 = s4 ++ s5 /\
        seq_forall_pair R s1 s4 /\
        seq_forall_pair R s2 s5.
Proof.
elim: s1 s2 s3 => [|a1 s1 IH] /=.
    move => s2 s3 Hforll25.
    exists [::], s3 => /=.
    split => //.
    split=> //.
    by apply: seq_forall_pair_empty.
move => s2 [|a3 s3].
    by rewrite seq_pair_forall_emptyr.
rewrite seq_forall_pair_cons => [[HR13 Hforall3]].
have := IH _ _ Hforall3.
move => [s4] [s5] [Heq] [Hforall14] Hforall25.
exists (a3::s4), s5.
by rewrite Heq seq_forall_pair_cons.
Qed.


Inductive SeqForallPair {A B} (R: A -> B -> Prop) : seq A -> seq B -> Prop :=
| SeqForallPair_empty: SeqForallPair R [::] [::]
| SeqForallPair_cons a b sa sb: R a b -> SeqForallPair R sa sb -> SeqForallPair R (a::sa) (b::sb).


Lemma SeqForallPair_in_forall1 A B (R: A -> B-> Prop) sa sb:
    SeqForallPair R sa sb -> seq_forall_pair R sa sb.
Proof.
elim => {sa sb} [| a b sa sb HR Hforall IH].
    by apply seq_forall_pair_empty.
by rewrite seq_forall_pair_cons.
Qed.

Lemma SeqForallPair_in_forall2 A B (R: A -> B-> Prop) sa sb:
    seq_forall_pair R sa sb -> SeqForallPair R sa sb.
Proof.
elim: sa sb => [|a sa IH] [|b sb] //;
    rewrite ?seq_pair_forall_emptyl ?seq_pair_forall_emptyr //.
    move => ?.
    by apply: SeqForallPair_empty.
rewrite seq_forall_pair_cons => [[HR Hforall]].
apply: SeqForallPair_cons => //.
by apply: IH.
Qed.

Lemma SeqForallPair_iff A B (R: A -> B-> Prop) sa sb:
    seq_forall_pair R sa sb <-> SeqForallPair R sa sb.
Proof.
split.
    by apply: SeqForallPair_in_forall2.
by apply: SeqForallPair_in_forall1.
Qed.

Lemma SeqForallPair_ext1 A B (R1 R2: A -> B -> Prop) l1 l2:
    (forall x y, R1 x y -> R2 x y) ->
    SeqForallPair R1 l1 l2 ->
    SeqForallPair R2 l1 l2.
Proof.
move => Hext.
elim => {l1 l2} => [|a b l1 l2 HRab Hforall12 IH12].
    by apply: SeqForallPair_empty.
apply: SeqForallPair_cons => //.
by apply: Hext.
Qed.

Lemma SeqForallPair_ext A B (R1 R2: A -> B -> Prop) l1 l2:
    (forall x y, R1 x y <-> R2 x y) ->
    SeqForallPair R1 l1 l2 <->
    SeqForallPair R2 l1 l2.
Proof.
move => Hext.
split;
apply: SeqForallPair_ext1 => x y;
by rewrite Hext.
Qed.

Lemma behead_rcons A (l: seq A) a b:
    behead (rcons (rcons l a) b) = rcons (behead (rcons l a)) b.
Proof.
by elim: l a b => [|c l IH] a b.
Qed.

Lemma rev_behead A (l: seq A) a:
(rev (behead (rev (a :: l)))) ++ [:: (last a l)] = a::l.
Proof.
elim: l a => [|a' l IH] a //=.
rewrite !rev_cons behead_rcons.
rewrite rev_rcons  -rev_cons /=.
by rewrite IH.
Qed.