From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export mathcomp.zify.zify.
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]

Require Import prosa.util.tactics.
Require Export prosa.util.supremum.

(** We define a few simple operations on lists that return zero for
    empty lists: [max0], [first0], and [last0]. *)
Definition max0 := foldl maxn 0.
Definition first0 := head 0.
Definition last0 := last 0.

(** Additional lemmas about [last0]. *)
Section Last0.

  (** Let [xs] be a non-empty sequence and [x] be an arbitrary element,
      then we prove that [last0 (x::xs) = last0 xs]. *)
  Lemma last0_cons :
    forall x xs,
      xs <> [::] ->
      last0 (x::xs) = last0 xs.
forall (x : nat) (xs : seq nat),
xs <> [::] -> last0 (x :: xs) = last0 xs
  Proof.
forall (x : nat) (xs : seq nat),
xs <> [::] -> last0 (x :: xs) = last0 xs by move=> x; elim. Qed.

  (** Similarly, let [xs_r] be a non-empty sequence and [xs_l] be any sequence,
      we prove that [last0 (xs_l ++ xs_r) = last0 xs_r]. *)
  Lemma last0_cat :
    forall xs_l xs_r,
      xs_r <> [::] ->
      last0 (xs_l ++ xs_r) = last0 xs_r.
forall xs_l xs_r : seq nat,
xs_r <> [::] -> last0 (xs_l ++ xs_r) = last0 xs_r
  Proof.
forall xs_l xs_r : seq nat,
xs_r <> [::] -> last0 (xs_l ++ xs_r) = last0 xs_r
    elim=> [//|xs xs_l IHxs_l] n NEQ.
xs: nat
xs_l: seq nat
IHxs_l: forall xs_r : seq nat,
xs_r <> [::] ->
last0 (xs_l ++ xs_r) = last0 xs_r
n: seq nat
NEQ: n <> [::]
last0 ((xs :: xs_l) ++ n) = last0 n
    simpl; rewrite last0_cons.
xs: nat
xs_l: seq nat
IHxs_l: forall xs_r : seq nat,
xs_r <> [::] ->
last0 (xs_l ++ xs_r) = last0 xs_r
n: seq nat
NEQ: n <> [::]
last0 (xs_l ++ n) = last0 n
xs: nat
xs_l: seq nat
IHxs_l: forall xs_r : seq nat,
xs_r <> [::] ->
last0 (xs_l ++ xs_r) = last0 xs_r
n: seq nat
NEQ: n <> [::]
xs_l ++ n <> [::]
    -
xs: nat
xs_l: seq nat
IHxs_l: forall xs_r : seq nat,
xs_r <> [::] ->
last0 (xs_l ++ xs_r) = last0 xs_r
n: seq nat
NEQ: n <> [::]
last0 (xs_l ++ n) = last0 n by apply IHxs_l.
    -
xs: nat
xs_l: seq nat
IHxs_l: forall xs_r : seq nat,
xs_r <> [::] ->
last0 (xs_l ++ xs_r) = last0 xs_r
n: seq nat
NEQ: n <> [::]
xs_l ++ n <> [::] by intros C; apply: NEQ; destruct xs_l.
  Qed.

  (** We also prove that [last0 xs = xs [| size xs -1 |] ]. *)
  Lemma last0_nth :
    forall xs,
      last0 xs = nth 0 xs (size xs).-1.
forall xs : seq nat, last0 xs = nth 0 xs (size xs).-1
  Proof.
forall xs : seq nat, last0 xs = nth 0 xs (size xs).-1 by intros; rewrite nth_last. Qed.

  (** We prove that for any non-empty sequence [xs] there is a sequence [xsh]
      such that [xsh ++ [::last0 x] = [xs]]. *)
  Lemma last0_ex_cat :
    forall x xs,
      xs <> [::] ->
      last0 xs = x ->
      exists xsh, xsh ++ [::x] = xs.
forall (x : nat) (xs : seq nat),
xs <> [::] ->
last0 xs = x ->
exists xsh : seq nat, xsh ++ [:: x] = xs
  Proof.
forall (x : nat) (xs : seq nat),
xs <> [::] ->
last0 xs = x ->
exists xsh : seq nat, xsh ++ [:: x] = xs
    move=> x; elim=> [//|a xs IHxs] NEQ LAST.
x, a: nat
xs: seq nat
IHxs: xs <> [::] ->
last0 xs = x ->
exists xsh : seq nat, xsh ++ [:: x] = xs
NEQ: a :: xs <> [::]
LAST: last0 (a :: xs) = x
exists xsh : seq nat, xsh ++ [:: x] = a :: xs
    destruct xs.
x, a: nat
IHxs: [::] <> [::] ->
last0 [::] = x ->
exists xsh : seq nat, xsh ++ [:: x] = [::]
NEQ: [:: a] <> [::]
LAST: last0 [:: a] = x
exists xsh : seq nat, xsh ++ [:: x] = [:: a]
x, a, n: nat
xs: seq nat
IHxs: n :: xs <> [::] ->
last0 (n :: xs) = x ->
exists xsh : seq nat, xsh ++ [:: x] = n :: xs
NEQ: [:: a, n & xs] <> [::]
LAST: last0 [:: a, n & xs] = x
exists xsh : seq nat, xsh ++ [:: x] = [:: a, n & xs]
    -
x, a: nat
IHxs: [::] <> [::] ->
last0 [::] = x ->
exists xsh : seq nat, xsh ++ [:: x] = [::]
NEQ: [:: a] <> [::]
LAST: last0 [:: a] = x
exists xsh : seq nat, xsh ++ [:: x] = [:: a] by exists [::]; move: LAST; rewrite /last0 /= => ->.
    -
x, a, n: nat
xs: seq nat
IHxs: n :: xs <> [::] ->
last0 (n :: xs) = x ->
exists xsh : seq nat, xsh ++ [:: x] = n :: xs
NEQ: [:: a, n & xs] <> [::]
LAST: last0 [:: a, n & xs] = x
exists xsh : seq nat, xsh ++ [:: x] = [:: a, n & xs] feed_n 2 IHxs; try by done.
x, a, n: nat
xs: seq nat
IHxs: exists xsh : seq nat, xsh ++ [:: x] = n :: xs
NEQ: [:: a, n & xs] <> [::]
LAST: last0 [:: a, n & xs] = x
exists xsh : seq nat, xsh ++ [:: x] = [:: a, n & xs]
      destruct IHxs as [xsh EQ].
x, a, n: nat
xs, xsh: seq nat
EQ: xsh ++ [:: x] = n :: xs
NEQ: [:: a, n & xs] <> [::]
LAST: last0 [:: a, n & xs] = x
exists xsh : seq nat, xsh ++ [:: x] = [:: a, n & xs]
      by exists (a::xsh); rewrite //= EQ.
  Qed.

  (** We prove that if [x] is the last element of a sequence [xs] and
      [x] satisfies a predicate, then [x] remains the last element in
      the filtered sequence. *)
  Lemma last0_filter :
    forall x xs (P : nat -> bool),
      xs <> [::] ->
      last0 xs = x ->
      P x ->
      last0 [seq x <- xs | P x] = x.
forall (x : nat) (xs : seq nat) (P : nat -> bool),
xs <> [::] ->
last0 xs = x -> P x -> last0 [seq x0 <- xs | P x0] = x
  Proof.
forall (x : nat) (xs : seq nat) (P : nat -> bool),
xs <> [::] ->
last0 xs = x -> P x -> last0 [seq x0 <- xs | P x0] = x
    clear; intros x xs P NEQ LAST PX.
x: nat
xs: seq nat
P: nat -> bool
NEQ: xs <> [::]
LAST: last0 xs = x
PX: P x
last0 [seq x <- xs | P x] = x
    destruct (last0_ex_cat x xs NEQ LAST) as [xsh EQ]; subst xs.
x: nat
P: nat -> bool
xsh: seq nat
LAST: last0 (xsh ++ [:: x]) = x
NEQ: xsh ++ [:: x] <> [::]
PX: P x
last0 [seq x <- xsh ++ [:: x] | P x] = x
    rewrite filter_cat last0_cat.
x: nat
P: nat -> bool
xsh: seq nat
LAST: last0 (xsh ++ [:: x]) = x
NEQ: xsh ++ [:: x] <> [::]
PX: P x
last0 [seq x <- [:: x] | P x] = x
x: nat
P: nat -> bool
xsh: seq nat
LAST: last0 (xsh ++ [:: x]) = x
NEQ: xsh ++ [:: x] <> [::]
PX: P x
[seq x <- [:: x] | P x] <> [::]
    all:rewrite //= PX //=.
  Qed.

End Last0.

(** Additional lemmas about [max0]. *)
Section Max0.

  (** First we prove that [max0 (x::xs)] is equal to [max {x, max0 xs}]. *)
  Lemma max0_cons : forall x xs, max0 (x :: xs) = maxn x (max0 xs).
forall (x : nat) (xs : seq nat),
max0 (x :: xs) = maxn x (max0 xs)
  Proof.
forall (x : nat) (xs : seq nat),
max0 (x :: xs) = maxn x (max0 xs) by move=> x xs; rewrite /max0 !foldlE /= !big_cons maxnCA. Qed.

  (** Next, we prove that if all the numbers of a seq [xs] are equal
      to a constant [k], then [max0 xs = k]. *)
  Lemma max0_of_uniform_set :
    forall k xs,
      size xs > 0 ->
      (forall x, x \in xs -> x = k) ->
      max0 xs = k.
forall (k : Datatypes_nat__canonical__eqtype_Equality)
  (xs : seq Datatypes_nat__canonical__eqtype_Equality),
0 < size xs ->
(forall x : Datatypes_nat__canonical__eqtype_Equality,
 x \in xs -> x = k) -> max0 xs = k
  Proof.
forall (k : Datatypes_nat__canonical__eqtype_Equality)
  (xs : seq Datatypes_nat__canonical__eqtype_Equality),
0 < size xs ->
(forall x : Datatypes_nat__canonical__eqtype_Equality,
 x \in xs -> x = k) -> max0 xs = k
    move=> k; elim=> [//|a xs IHxs] SIZE ALL.
k, a: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: 0 < size xs ->
(forall
   x : Datatypes_nat__canonical__eqtype_Equality,
 x \in xs -> x = k) -> max0 xs = k
SIZE: 0 < size (a :: xs)
ALL: forall
  x : Datatypes_nat__canonical__eqtype_Equality,
x \in a :: xs -> x = k
max0 (a :: xs) = k
    destruct xs as [|b xs].
k, a: Datatypes_nat__canonical__eqtype_Equality
IHxs: 0 < size [::] ->
(forall
   x : Datatypes_nat__canonical__eqtype_Equality,
 x \in [::] -> x = k) -> 
max0 [::] = k
SIZE: 0 < size [:: a]
ALL: forall
  x : Datatypes_nat__canonical__eqtype_Equality,
x \in [:: a] -> x = k
max0 [:: a] = k
k, a, b: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: 0 < size (b :: xs) ->
(forall
   x : Datatypes_nat__canonical__eqtype_Equality,
 x \in b :: xs -> x = k) -> 
max0 (b :: xs) = k
SIZE: 0 < size [:: a, b & xs]
ALL: forall
  x : Datatypes_nat__canonical__eqtype_Equality,
x \in [:: a, b & xs] -> x = k
max0 [:: a, b & xs] = k
    -
k, a: Datatypes_nat__canonical__eqtype_Equality
IHxs: 0 < size [::] ->
(forall
   x : Datatypes_nat__canonical__eqtype_Equality,
 x \in [::] -> x = k) -> 
max0 [::] = k
SIZE: 0 < size [:: a]
ALL: forall
  x : Datatypes_nat__canonical__eqtype_Equality,
x \in [:: a] -> x = k
max0 [:: a] = k rewrite /max0 //= max0n; apply ALL.
k, a: Datatypes_nat__canonical__eqtype_Equality
IHxs: 0 < size [::] ->
(forall
   x : Datatypes_nat__canonical__eqtype_Equality,
 x \in [::] -> x = k) -> 
max0 [::] = k
SIZE: 0 < size [:: a]
ALL: forall
  x : Datatypes_nat__canonical__eqtype_Equality,
x \in [:: a] -> x = k
a \in [:: a]
      by rewrite in_cons; apply/orP; left.
    -
k, a, b: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: 0 < size (b :: xs) ->
(forall
   x : Datatypes_nat__canonical__eqtype_Equality,
 x \in b :: xs -> x = k) -> 
max0 (b :: xs) = k
SIZE: 0 < size [:: a, b & xs]
ALL: forall
  x : Datatypes_nat__canonical__eqtype_Equality,
x \in [:: a, b & xs] -> x = k
max0 [:: a, b & xs] = k rewrite max0_cons IHxs; [ | by done | ].
k, a, b: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: 0 < size (b :: xs) ->
(forall
   x : Datatypes_nat__canonical__eqtype_Equality,
 x \in b :: xs -> x = k) -> 
max0 (b :: xs) = k
SIZE: 0 < size [:: a, b & xs]
ALL: forall
  x : Datatypes_nat__canonical__eqtype_Equality,
x \in [:: a, b & xs] -> x = k
maxn a k = k
k, a, b: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: 0 < size (b :: xs) ->
(forall
   x : Datatypes_nat__canonical__eqtype_Equality,
 x \in b :: xs -> x = k) -> 
max0 (b :: xs) = k
SIZE: 0 < size [:: a, b & xs]
ALL: forall
  x : Datatypes_nat__canonical__eqtype_Equality,
x \in [:: a, b & xs] -> x = k
forall x : Datatypes_nat__canonical__eqtype_Equality,
x \in b :: xs -> x = k
      +
k, a, b: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: 0 < size (b :: xs) ->
(forall
   x : Datatypes_nat__canonical__eqtype_Equality,
 x \in b :: xs -> x = k) -> 
max0 (b :: xs) = k
SIZE: 0 < size [:: a, b & xs]
ALL: forall
  x : Datatypes_nat__canonical__eqtype_Equality,
x \in [:: a, b & xs] -> x = k
maxn a k = k by rewrite [a]ALL; [ rewrite maxnn | rewrite in_cons; apply/orP; left].
      +
k, a, b: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: 0 < size (b :: xs) ->
(forall
   x : Datatypes_nat__canonical__eqtype_Equality,
 x \in b :: xs -> x = k) -> 
max0 (b :: xs) = k
SIZE: 0 < size [:: a, b & xs]
ALL: forall
  x : Datatypes_nat__canonical__eqtype_Equality,
x \in [:: a, b & xs] -> x = k
forall x : Datatypes_nat__canonical__eqtype_Equality,
x \in b :: xs -> x = k move=> x H; apply ALL.
k, a, b: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: 0 < size (b :: xs) ->
(forall
   x : Datatypes_nat__canonical__eqtype_Equality,
 x \in b :: xs -> x = k) -> 
max0 (b :: xs) = k
SIZE: 0 < size [:: a, b & xs]
ALL: forall
  x : Datatypes_nat__canonical__eqtype_Equality,
x \in [:: a, b & xs] -> x = k
x: Datatypes_nat__canonical__eqtype_Equality
H: x \in b :: xs
x \in [:: a, b & xs]
        rewrite in_cons; move: H => /orP [/eqP EQ | IN].
k, a, b: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: 0 < size (b :: xs) ->
(forall
   x : Datatypes_nat__canonical__eqtype_Equality,
 x \in b :: xs -> x = k) -> 
max0 (b :: xs) = k
SIZE: 0 < size [:: a, b & xs]
ALL: forall
  x : Datatypes_nat__canonical__eqtype_Equality,
x \in [:: a, b & xs] -> x = k
x: Datatypes_nat__canonical__eqtype_Equality
EQ: x = b
(x == a) || (x \in b :: xs)
k, a, b: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: 0 < size (b :: xs) ->
(forall
   x : Datatypes_nat__canonical__eqtype_Equality,
 x \in b :: xs -> x = k) -> 
max0 (b :: xs) = k
SIZE: 0 < size [:: a, b & xs]
ALL: forall
  x : Datatypes_nat__canonical__eqtype_Equality,
x \in [:: a, b & xs] -> x = k
x: Datatypes_nat__canonical__eqtype_Equality
IN: (fix mem_seq
   (s : seq
          Datatypes_nat__canonical__eqtype_Equality) :
     Datatypes_nat__canonical__eqtype_Equality ->
     bool :=
   match s with
   | [::] => xpred0
   | y :: s' =>
       fun
         x : Datatypes_nat__canonical__eqtype_Equality
       => (x == y) || mem_seq s' x
   end) xs x
(x == a) || (x \in b :: xs)
        *
k, a, b: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: 0 < size (b :: xs) ->
(forall
   x : Datatypes_nat__canonical__eqtype_Equality,
 x \in b :: xs -> x = k) -> 
max0 (b :: xs) = k
SIZE: 0 < size [:: a, b & xs]
ALL: forall
  x : Datatypes_nat__canonical__eqtype_Equality,
x \in [:: a, b & xs] -> x = k
x: Datatypes_nat__canonical__eqtype_Equality
EQ: x = b
(x == a) || (x \in b :: xs) by subst x; rewrite !in_cons; apply/orP; right; apply/orP; left.
        *
k, a, b: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: 0 < size (b :: xs) ->
(forall
   x : Datatypes_nat__canonical__eqtype_Equality,
 x \in b :: xs -> x = k) -> 
max0 (b :: xs) = k
SIZE: 0 < size [:: a, b & xs]
ALL: forall
  x : Datatypes_nat__canonical__eqtype_Equality,
x \in [:: a, b & xs] -> x = k
x: Datatypes_nat__canonical__eqtype_Equality
IN: (fix mem_seq
   (s : seq
          Datatypes_nat__canonical__eqtype_Equality) :
     Datatypes_nat__canonical__eqtype_Equality ->
     bool :=
   match s with
   | [::] => xpred0
   | y :: s' =>
       fun
         x : Datatypes_nat__canonical__eqtype_Equality
       => (x == y) || mem_seq s' x
   end) xs x
(x == a) || (x \in b :: xs) by rewrite !in_cons; apply/orP; right; apply/orP; right.
  Qed.

  (** We prove that no element in a sequence [xs] is greater than [max0 xs]. *)
  Lemma in_max0_le :
    forall xs x, x \in xs -> x <= max0 xs.
forall
  (xs : seq_predType
          Datatypes_nat__canonical__eqtype_Equality)
  (x : nat), x \in xs -> x <= max0 xs
  Proof.
forall
  (xs : seq_predType
          Datatypes_nat__canonical__eqtype_Equality)
  (x : nat), x \in xs -> x <= max0 xs
    elim=> [//|a xs IHxs] x.
a: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: forall x : nat, x \in xs -> x <= max0 xs
x: nat
x \in a :: xs -> x <= max0 (a :: xs)
    rewrite in_cons; move => /orP [/eqP EQ | IN]; subst.
a: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: forall x : nat, x \in xs -> x <= max0 xs
a <= max0 (a :: xs)
a: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: forall x : nat, x \in xs -> x <= max0 xs
x: nat
IN: x \in xs
x <= max0 (a :: xs)
    -
a: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: forall x : nat, x \in xs -> x <= max0 xs
a <= max0 (a :: xs) by rewrite !max0_cons leq_maxl.
    -
a: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: forall x : nat, x \in xs -> x <= max0 xs
x: nat
IN: x \in xs
x <= max0 (a :: xs) apply leq_trans with (max0 xs); first by eauto.
a: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: forall x : nat, x \in xs -> x <= max0 xs
x: nat
IN: x \in xs
max0 xs <= max0 (a :: xs)
      by rewrite max0_cons; apply leq_maxr.
  Qed.

  (** We prove that for a non-empty sequence [xs], [max0 xs ∈ xs]. *)
  Lemma max0_in_seq :
    forall xs,
      xs <> [::] ->
      max0 xs \in xs.
forall xs : seq nat, xs <> [::] -> max0 xs \in xs
  Proof.
forall xs : seq nat, xs <> [::] -> max0 xs \in xs
    elim=> [//|a xs IHxs] _.
a: nat
xs: seq nat
IHxs: xs <> [::] -> max0 xs \in xs
max0 (a :: xs) \in a :: xs
    destruct xs as [|n xs].
a: nat
IHxs: [::] <> [::] -> max0 [::] \in [::]
max0 [:: a] \in [:: a]
a, n: nat
xs: seq nat
IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
max0 [:: a, n & xs] \in [:: a, n & xs]
    -
a: nat
IHxs: [::] <> [::] -> max0 [::] \in [::]
max0 [:: a] \in [:: a] destruct a; simpl; first by done.
a: nat
IHxs: [::] <> [::] -> max0 [::] \in [::]
max0 [:: a.+1] \in [:: a.+1]
      by rewrite /max0 //= max0n in_cons eq_refl.
    -
a, n: nat
xs: seq nat
IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
max0 [:: a, n & xs] \in [:: a, n & xs] rewrite max0_cons.
a, n: nat
xs: seq nat
IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
maxn a (max0 (n :: xs)) \in [:: a, n & xs]
      move: (leq_total a (max0 (n::xs))) => /orP [LE|LE].
a, n: nat
xs: seq nat
IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
LE: a <= max0 (n :: xs)
maxn a (max0 (n :: xs)) \in [:: a, n & xs]
a, n: nat
xs: seq nat
IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
LE: max0 (n :: xs) <= a
maxn a (max0 (n :: xs)) \in [:: a, n & xs]
      +
a, n: nat
xs: seq nat
IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
LE: a <= max0 (n :: xs)
maxn a (max0 (n :: xs)) \in [:: a, n & xs] by rewrite maxnE subnKC // in_cons; apply/orP; right; apply IHxs.
      +
a, n: nat
xs: seq nat
IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
LE: max0 (n :: xs) <= a
maxn a (max0 (n :: xs)) \in [:: a, n & xs] rewrite maxnE; move: LE; rewrite -subn_eq0; move => /eqP EQ.
a, n: nat
xs: seq nat
IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
EQ: max0 (n :: xs) - a = 0
a + (max0 (n :: xs) - a) \in [:: a, n & xs]
        by rewrite EQ addn0 in_cons; apply/orP; left.
  Qed.

  (** We prove a technical lemma stating that one can remove
      duplicating element from the head of a sequence. *)
  Lemma max0_2cons_eq :
    forall x xs,
      max0 (x::x::xs) = max0 (x::xs).
forall (x : nat) (xs : seq nat),
max0 [:: x, x & xs] = max0 (x :: xs)
  Proof.
forall (x : nat) (xs : seq nat),
max0 [:: x, x & xs] = max0 (x :: xs) by intros; rewrite !max0_cons maxnA maxnn. Qed.

  (** Similarly, we prove that one can remove the first element of a
      sequence if it is not greater than the second element of this
      sequence. *)
  Lemma max0_2cons_le :
    forall x1 x2 xs,
      x1 <= x2 ->
      max0 (x1::x2::xs) = max0 (x2::xs).
forall (x1 x2 : nat) (xs : seq nat),
x1 <= x2 -> max0 [:: x1, x2 & xs] = max0 (x2 :: xs)
  Proof.
forall (x1 x2 : nat) (xs : seq nat),
x1 <= x2 -> max0 [:: x1, x2 & xs] = max0 (x2 :: xs)
    by move=> x1 x2 ? ?; rewrite !max0_cons maxnA [maxn x1 x2]maxnE subnKC.
  Qed.

  (** We prove that [max0] of a sequence [xs]
      is equal to [max0] of sequence [xs] without 0s. *)
  Lemma max0_rem0 :
    forall xs,
      max0 ([seq x <- xs | 0 < x]) = max0 xs.
forall xs : seq nat,
max0 [seq x <- xs | 0 < x] = max0 xs
  Proof.
forall xs : seq nat,
max0 [seq x <- xs | 0 < x] = max0 xs
    elim=> [//|a xs IHxs].
a: nat
xs: seq nat
IHxs: max0 [seq x <- xs | 0 < x] = max0 xs
max0 [seq x <- a :: xs | 0 < x] = max0 (a :: xs)
    simpl; destruct a; simpl.
xs: seq nat
IHxs: max0 [seq x <- xs | 0 < x] = max0 xs
max0 [seq x <- xs | 0 < x] = max0 (0 :: xs)
a: nat
xs: seq nat
IHxs: max0 [seq x <- xs | 0 < x] = max0 xs
max0 (a.+1 :: [seq x <- xs | 0 < x]) =
max0 (a.+1 :: xs)
    -
xs: seq nat
IHxs: max0 [seq x <- xs | 0 < x] = max0 xs
max0 [seq x <- xs | 0 < x] = max0 (0 :: xs) by rewrite max0_cons max0n.
    -
a: nat
xs: seq nat
IHxs: max0 [seq x <- xs | 0 < x] = max0 xs
max0 (a.+1 :: [seq x <- xs | 0 < x]) =
max0 (a.+1 :: xs) by rewrite !max0_cons IHxs.
  Qed.

  (** Note that the last element is at most the max element. *)
  Lemma last_of_seq_le_max_of_seq:
    forall xs, last0 xs <= max0 xs.
forall xs : seq nat, last0 xs <= max0 xs
  Proof.
forall xs : seq nat, last0 xs <= max0 xs
    intros xs.
xs: seq nat
last0 xs <= max0 xs
    have EX: exists len, size xs <= len.
xs: seq nat
exists len : nat, size xs <= len
xs: seq nat
EX: exists len : nat, size xs <= len
last0 xs <= max0 xs
    {
xs: seq nat
exists len : nat, size xs <= len by exists (size xs). }
xs: seq nat
EX: exists len : nat, size xs <= len
last0 xs <= max0 xs
    move: EX => [len LE].
xs: seq nat
len: nat
LE: size xs <= len
last0 xs <= max0 xs
    generalize dependent xs; elim: len => [|n IHlen] xs LE.
xs: seq nat
LE: size xs <= 0
last0 xs <= max0 xs
n: nat
IHlen: forall xs : seq nat,
size xs <= n -> last0 xs <= max0 xs
xs: seq nat
LE: size xs <= n.+1
last0 xs <= max0 xs
    -
xs: seq nat
LE: size xs <= 0
last0 xs <= max0 xs by intros; move: LE; rewrite leqn0 size_eq0; move => /eqP EQ; subst.
    -
n: nat
IHlen: forall xs : seq nat,
size xs <= n -> last0 xs <= max0 xs
xs: seq nat
LE: size xs <= n.+1
last0 xs <= max0 xs move: LE; rewrite leq_eqVlt; move => /orP [/eqP EQ| LE]; last by apply IHlen.
n: nat
IHlen: forall xs : seq nat,
size xs <= n -> last0 xs <= max0 xs
xs: seq nat
EQ: size xs = n.+1
last0 xs <= max0 xs
      destruct xs as [ | x1 xs]; first by inversion EQ.
n: nat
IHlen: forall xs : seq nat,
size xs <= n -> last0 xs <= max0 xs
x1: nat
xs: seq nat
EQ: size (x1 :: xs) = n.+1
last0 (x1 :: xs) <= max0 (x1 :: xs)
      destruct xs as [ | x2 xs]; first by rewrite /max leq_max; apply/orP; right.
n: nat
IHlen: forall xs : seq nat,
size xs <= n -> last0 xs <= max0 xs
x1, x2: nat
xs: seq nat
EQ: size [:: x1, x2 & xs] = n.+1
last0 [:: x1, x2 & xs] <= max0 [:: x1, x2 & xs]
      have ->: last0 [:: x1, x2 & xs] = last0 [:: x2 & xs] by done.
n: nat
IHlen: forall xs : seq nat,
size xs <= n -> last0 xs <= max0 xs
x1, x2: nat
xs: seq nat
EQ: size [:: x1, x2 & xs] = n.+1
last0 (x2 :: xs) <= max0 [:: x1, x2 & xs]
      rewrite max0_cons leq_max; apply/orP; right; apply IHlen.
n: nat
IHlen: forall xs : seq nat,
size xs <= n -> last0 xs <= max0 xs
x1, x2: nat
xs: seq nat
EQ: size [:: x1, x2 & xs] = n.+1
size (x2 :: xs) <= n
      move: EQ => /eqP; simpl; rewrite eqSS; move => /eqP EQ.
n: nat
IHlen: forall xs : seq nat,
size xs <= n -> last0 xs <= max0 xs
x1, x2: nat
xs: seq nat
EQ: (size xs).+1 = n
size xs < n
      by subst.
  Qed.

  (** Let's introduce the notion of the nth element of a sequence. *)
  Notation "xs [| n |]" := (nth 0 xs n) (at level 30).

  (** If any element of a sequence [xs] is less-than-or-equal-to
      the corresponding element of a sequence [ys], then [max0] of
      [xs] is less-than-or-equal-to max of [ys]. *)
  Lemma max_of_dominating_seq :
    forall xs ys,
      (forall n, xs[|n|] <= ys[|n|]) ->
      max0 xs <= max0 ys.
forall xs ys : seq nat,
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
  Proof.
forall xs ys : seq nat,
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
    intros xs ys.
xs, ys: seq nat
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
    have EX: exists len, size xs <= len /\ size ys <= len.
xs, ys: seq nat
exists len : nat, size xs <= len /\ size ys <= len
xs, ys: seq nat
EX: exists len : nat,
  size xs <= len /\ size ys <= len
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
    {
xs, ys: seq nat
exists len : nat, size xs <= len /\ size ys <= len exists (maxn (size xs) (size ys)).
xs, ys: seq nat
size xs <= maxn (size xs) (size ys) /\
size ys <= maxn (size xs) (size ys)
      by split; rewrite leq_max; apply/orP; [left | right].
    }
xs, ys: seq nat
EX: exists len : nat,
  size xs <= len /\ size ys <= len
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
    move: EX => [len [LE1 LE2]].
xs, ys: seq nat
len: nat
LE1: size xs <= len
LE2: size ys <= len
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
    generalize dependent xs; generalize dependent ys.
len: nat
forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
    elim: len => [ | len IHlen] xs LE1 ys LE2.
xs: seq nat
LE1: size xs <= 0
ys: seq nat
LE2: size ys <= 0
(forall n : nat, ys [|n|] <= xs [|n|]) ->
max0 ys <= max0 xs
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
xs: seq nat
LE1: size xs <= len.+1
ys: seq nat
LE2: size ys <= len.+1
(forall n : nat, ys [|n|] <= xs [|n|]) ->
max0 ys <= max0 xs
    {
xs: seq nat
LE1: size xs <= 0
ys: seq nat
LE2: size ys <= 0
(forall n : nat, ys [|n|] <= xs [|n|]) ->
max0 ys <= max0 xs by move: LE1 LE2; rewrite !leqn0 !size_eq0; move => /eqP E1 /eqP E2; subst. }
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
xs: seq nat
LE1: size xs <= len.+1
ys: seq nat
LE2: size ys <= len.+1
(forall n : nat, ys [|n|] <= xs [|n|]) ->
max0 ys <= max0 xs
    {
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
xs: seq nat
LE1: size xs <= len.+1
ys: seq nat
LE2: size ys <= len.+1
(forall n : nat, ys [|n|] <= xs [|n|]) ->
max0 ys <= max0 xs move: xs ys LE1 LE2 => [ |x xs] [//|y ys] LE1 LE2 H.
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
y: nat
ys: seq nat
LE1: size [::] <= len.+1
LE2: size (y :: ys) <= len.+1
H: forall n : nat, (y :: ys) [|n|] <= [::] [|n|]
max0 (y :: ys) <= max0 [::]
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
x: nat
xs: seq nat
y: nat
ys: seq nat
LE1: size (x :: xs) <= len.+1
LE2: size (y :: ys) <= len.+1
H: forall n : nat, (y :: ys) [|n|] <= (x :: xs) [|n|]
max0 (y :: ys) <= max0 (x :: xs)
      {
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
y: nat
ys: seq nat
LE1: size [::] <= len.+1
LE2: size (y :: ys) <= len.+1
H: forall n : nat, (y :: ys) [|n|] <= [::] [|n|]
max0 (y :: ys) <= max0 [::] have L: forall xs, (forall n, xs [| n |] = 0) -> max0 xs = 0.
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
y: nat
ys: seq nat
LE1: size [::] <= len.+1
LE2: size (y :: ys) <= len.+1
H: forall n : nat, (y :: ys) [|n|] <= [::] [|n|]
forall xs : seq nat,
(forall n : nat, xs [|n|] = 0) -> max0 xs = 0
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
y: nat
ys: seq nat
LE1: size [::] <= len.+1
LE2: size (y :: ys) <= len.+1
H: forall n : nat, (y :: ys) [|n|] <= [::] [|n|]
L: forall xs : seq nat,
(forall n : nat, xs [|n|] = 0) -> max0 xs = 0
max0 (y :: ys) <= max0 [::]
        {
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
y: nat
ys: seq nat
LE1: size [::] <= len.+1
LE2: size (y :: ys) <= len.+1
H: forall n : nat, (y :: ys) [|n|] <= [::] [|n|]
forall xs : seq nat,
(forall n : nat, xs [|n|] = 0) -> max0 xs = 0 clear; elim=> [//|x xs IHxs] H.
x: nat
xs: seq nat
IHxs: (forall n : nat, xs [|n|] = 0) -> max0 xs = 0
H: forall n : nat, (x :: xs) [|n|] = 0
max0 (x :: xs) = 0
          rewrite max0_cons.
x: nat
xs: seq nat
IHxs: (forall n : nat, xs [|n|] = 0) -> max0 xs = 0
H: forall n : nat, (x :: xs) [|n|] = 0
maxn x (max0 xs) = 0
          apply/eqP; rewrite eqn_leq; apply/andP; split; last by done.
x: nat
xs: seq nat
IHxs: (forall n : nat, xs [|n|] = 0) -> max0 xs = 0
H: forall n : nat, (x :: xs) [|n|] = 0
maxn x (max0 xs) <= 0
          rewrite geq_max; apply/andP; split.
x: nat
xs: seq nat
IHxs: (forall n : nat, xs [|n|] = 0) -> max0 xs = 0
H: forall n : nat, (x :: xs) [|n|] = 0
x <= 0
x: nat
xs: seq nat
IHxs: (forall n : nat, xs [|n|] = 0) -> max0 xs = 0
H: forall n : nat, (x :: xs) [|n|] = 0
max0 xs <= 0
          -
x: nat
xs: seq nat
IHxs: (forall n : nat, xs [|n|] = 0) -> max0 xs = 0
H: forall n : nat, (x :: xs) [|n|] = 0
x <= 0 by specialize (H 0); simpl in H; rewrite H.
          -
x: nat
xs: seq nat
IHxs: (forall n : nat, xs [|n|] = 0) -> max0 xs = 0
H: forall n : nat, (x :: xs) [|n|] = 0
max0 xs <= 0 rewrite leqn0; apply/eqP; apply: IHxs.
x: nat
xs: seq nat
H: forall n : nat, (x :: xs) [|n|] = 0
forall n : nat, xs [|n|] = 0
            by move=> n; specialize (H n.+1); simpl in H.
        }
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
y: nat
ys: seq nat
LE1: size [::] <= len.+1
LE2: size (y :: ys) <= len.+1
H: forall n : nat, (y :: ys) [|n|] <= [::] [|n|]
L: forall xs : seq nat,
(forall n : nat, xs [|n|] = 0) -> max0 xs = 0
max0 (y :: ys) <= max0 [::]
        rewrite L; first by done.
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
y: nat
ys: seq nat
LE1: size [::] <= len.+1
LE2: size (y :: ys) <= len.+1
H: forall n : nat, (y :: ys) [|n|] <= [::] [|n|]
L: forall xs : seq nat,
(forall n : nat, xs [|n|] = 0) -> max0 xs = 0
forall n : nat, (y :: ys) [|n|] = 0
        move=> n0; specialize (H n0).
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
y: nat
ys: seq nat
LE1: size [::] <= len.+1
LE2: size (y :: ys) <= len.+1
n0: nat
H: (y :: ys) [|n0|] <= [::] [|n0|]
L: forall xs : seq nat,
(forall n : nat, xs [|n|] = 0) -> max0 xs = 0
(y :: ys) [|n0|] = 0
        by destruct n0; simpl in *; apply/eqP; rewrite -leqn0.
      }
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
x: nat
xs: seq nat
y: nat
ys: seq nat
LE1: size (x :: xs) <= len.+1
LE2: size (y :: ys) <= len.+1
H: forall n : nat, (y :: ys) [|n|] <= (x :: xs) [|n|]
max0 (y :: ys) <= max0 (x :: xs)
      {
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
x: nat
xs: seq nat
y: nat
ys: seq nat
LE1: size (x :: xs) <= len.+1
LE2: size (y :: ys) <= len.+1
H: forall n : nat, (y :: ys) [|n|] <= (x :: xs) [|n|]
max0 (y :: ys) <= max0 (x :: xs) rewrite !max0_cons geq_max; apply/andP; split.
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
x: nat
xs: seq nat
y: nat
ys: seq nat
LE1: size (x :: xs) <= len.+1
LE2: size (y :: ys) <= len.+1
H: forall n : nat, (y :: ys) [|n|] <= (x :: xs) [|n|]
y <= maxn x (max0 xs)
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
x: nat
xs: seq nat
y: nat
ys: seq nat
LE1: size (x :: xs) <= len.+1
LE2: size (y :: ys) <= len.+1
H: forall n : nat, (y :: ys) [|n|] <= (x :: xs) [|n|]
max0 ys <= maxn x (max0 xs)
        +
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
x: nat
xs: seq nat
y: nat
ys: seq nat
LE1: size (x :: xs) <= len.+1
LE2: size (y :: ys) <= len.+1
H: forall n : nat, (y :: ys) [|n|] <= (x :: xs) [|n|]
y <= maxn x (max0 xs) rewrite leq_max; apply/orP; left.
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
x: nat
xs: seq nat
y: nat
ys: seq nat
LE1: size (x :: xs) <= len.+1
LE2: size (y :: ys) <= len.+1
H: forall n : nat, (y :: ys) [|n|] <= (x :: xs) [|n|]
y <= x
          by specialize (H 0); simpl in H.
        +
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
x: nat
xs: seq nat
y: nat
ys: seq nat
LE1: size (x :: xs) <= len.+1
LE2: size (y :: ys) <= len.+1
H: forall n : nat, (y :: ys) [|n|] <= (x :: xs) [|n|]
max0 ys <= maxn x (max0 xs) rewrite leq_max; apply/orP; right.
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
x: nat
xs: seq nat
y: nat
ys: seq nat
LE1: size (x :: xs) <= len.+1
LE2: size (y :: ys) <= len.+1
H: forall n : nat, (y :: ys) [|n|] <= (x :: xs) [|n|]
max0 ys <= max0 xs
          apply IHlen; try (by rewrite ltnS in LE1, LE2).
len: nat
IHlen: forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
(forall n : nat, xs [|n|] <= ys [|n|]) ->
max0 xs <= max0 ys
x: nat
xs: seq nat
y: nat
ys: seq nat
LE1: size (x :: xs) <= len.+1
LE2: size (y :: ys) <= len.+1
H: forall n : nat, (y :: ys) [|n|] <= (x :: xs) [|n|]
forall n : nat, ys [|n|] <= xs [|n|]
          by move=> n1; specialize (H n1.+1); simpl in H.
      }
    }
  Qed.

End Max0.

(** Additional lemmas about [rem] for lists. *)
Section RemList.

  (** We prove that if [x] lies in [xs] excluding [y], then
      [x] also lies in [xs]. *)
  Lemma rem_in :
    forall {X : eqType} (x y : X) (xs : seq X),
      x \in rem y xs -> x \in xs.
forall (X : eqType) (x y : X) (xs : seq X),
x \in rem (T:=X) y xs -> x \in xs
  Proof.
forall (X : eqType) (x y : X) (xs : seq X),
x \in rem (T:=X) y xs -> x \in xs
    move=> X x y; elim=> [|a xs IHxs] /= H.
X: eqType
x, y: X
H: x \in [::]
x \in [::]
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in rem (T:=X) y xs -> x \in xs
H: x
  \in (if a == y then xs else a :: rem (T:=X) y xs)
x \in a :: xs
    {
X: eqType
x, y: X
H: x \in [::]
x \in [::] by rewrite in_nil in H. }
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in rem (T:=X) y xs -> x \in xs
H: x
  \in (if a == y then xs else a :: rem (T:=X) y xs)
x \in a :: xs
    {
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in rem (T:=X) y xs -> x \in xs
H: x
  \in (if a == y then xs else a :: rem (T:=X) y xs)
x \in a :: xs rewrite in_cons; apply/orP.
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in rem (T:=X) y xs -> x \in xs
H: x
  \in (if a == y then xs else a :: rem (T:=X) y xs)
x == a \/ x \in xs
      destruct (a == y) eqn:EQ.
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in rem (T:=X) y xs -> x \in xs
EQ: (a == y) = true
H: x \in xs
x == a \/ x \in xs
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in rem (T:=X) y xs -> x \in xs
EQ: (a == y) = false
H: x \in a :: rem (T:=X) y xs
x == a \/ x \in xs
      {
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in rem (T:=X) y xs -> x \in xs
EQ: (a == y) = true
H: x \in xs
x == a \/ x \in xs by move: EQ => /eqP EQ; subst a; right. }
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in rem (T:=X) y xs -> x \in xs
EQ: (a == y) = false
H: x \in a :: rem (T:=X) y xs
x == a \/ x \in xs
      {
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in rem (T:=X) y xs -> x \in xs
EQ: (a == y) = false
H: x \in a :: rem (T:=X) y xs
x == a \/ x \in xs move: H; rewrite in_cons; move => /orP [/eqP H | H].
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in rem (T:=X) y xs -> x \in xs
EQ: (a == y) = false
H: x = a
x == a \/ x \in xs
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in rem (T:=X) y xs -> x \in xs
EQ: (a == y) = false
H: x \in rem (T:=X) y xs
x == a \/ x \in xs
        -
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in rem (T:=X) y xs -> x \in xs
EQ: (a == y) = false
H: x = a
x == a \/ x \in xs by subst a; left.
        -
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in rem (T:=X) y xs -> x \in xs
EQ: (a == y) = false
H: x \in rem (T:=X) y xs
x == a \/ x \in xs by right; apply IHxs.
      }
    }
  Qed.

  (** Similarly, we prove that if [x <> y] and [x] lies in [xs],
      then [x] lies in [xs] excluding [y]. *)
  Lemma in_neq_impl_rem_in :
    forall {X : eqType} (x y : X) (xs : seq X),
      x \in xs ->
      x != y ->
      x \in rem y xs.
forall (X : eqType) (x y : X) (xs : seq X),
x \in xs -> x != y -> x \in rem (T:=X) y xs
  Proof.
forall (X : eqType) (x y : X) (xs : seq X),
x \in xs -> x != y -> x \in rem (T:=X) y xs
    move=> X x y; elim=> [//|a xs IHxs].
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs
x \in a :: xs ->
x != y -> x \in rem (T:=X) y (a :: xs)
    rewrite in_cons => /orP [/eqP EQ | IN]; intros NEQ.
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs
EQ: x = a
NEQ: x != y
x \in rem (T:=X) y (a :: xs)
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs
IN: x \in xs
NEQ: x != y
x \in rem (T:=X) y (a :: xs)
    {
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs
EQ: x = a
NEQ: x != y
x \in rem (T:=X) y (a :: xs) rewrite -EQ //=.
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs
EQ: x = a
NEQ: x != y
x \in (if x == y then xs else x :: rem (T:=X) y xs)
      move: NEQ; rewrite -eqbF_neg => /eqP ->.
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs
EQ: x = a
x \in x :: rem (T:=X) y xs
      by rewrite in_cons; apply/orP; left.
    }
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs
IN: x \in xs
NEQ: x != y
x \in rem (T:=X) y (a :: xs)
    {
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs
IN: x \in xs
NEQ: x != y
x \in rem (T:=X) y (a :: xs) simpl; destruct (a == y) eqn:AD; first by done.
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs
IN: x \in xs
NEQ: x != y
AD: (a == y) = false
x \in a :: rem (T:=X) y xs
      rewrite in_cons; apply/orP; right.
X: eqType
x, y, a: X
xs: seq X
IHxs: x \in xs -> x != y -> x \in rem (T:=X) y xs
IN: x \in xs
NEQ: x != y
AD: (a == y) = false
x \in rem (T:=X) y xs
      by apply IHxs.
    }
  Qed.

  (** We prove that if we remove an element [x] for which [P x] from a
      filter, then the size of the filter decreases by [1]. *)
  Lemma filter_size_rem :
    forall {X : eqType} (x : X) (xs : seq X) (P : pred X),
      (x \in xs) ->
      P x ->
      size [seq y <- xs | P y] = size [seq y <- rem x xs | P y] + 1.
forall (X : eqType) (x : X) (xs : seq X) (P : pred X),
x \in xs ->
P x ->
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
  Proof.
forall (X : eqType) (x : X) (xs : seq X) (P : pred X),
x \in xs ->
P x ->
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
    move=> X x + P + H0; elim=> [|a xs IHxs] H; first by inversion H.
X: eqType
x: X
P: pred X
H0: P x
a: X
xs: seq X
IHxs: x \in xs ->
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
H: x \in a :: xs
size [seq y <- a :: xs | P y] =
size [seq y <- rem (T:=X) x (a :: xs) | P y] + 1
    move: H; rewrite in_cons; move => /orP [/eqP H | H]; subst.
X: eqType
P: pred X
a: X
H0: P a
xs: seq X
IHxs: a \in xs ->
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) a xs | P y] + 1
size [seq y <- a :: xs | P y] =
size [seq y <- rem (T:=X) a (a :: xs) | P y] + 1
X: eqType
x: X
P: pred X
H0: P x
a: X
xs: seq X
IHxs: x \in xs ->
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
H: x \in xs
size [seq y <- a :: xs | P y] =
size [seq y <- rem (T:=X) x (a :: xs) | P y] + 1
    {
X: eqType
P: pred X
a: X
H0: P a
xs: seq X
IHxs: a \in xs ->
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) a xs | P y] + 1
size [seq y <- a :: xs | P y] =
size [seq y <- rem (T:=X) a (a :: xs) | P y] + 1 by simpl; rewrite H0 -[X in X = _]addn1 eq_refl. }
X: eqType
x: X
P: pred X
H0: P x
a: X
xs: seq X
IHxs: x \in xs ->
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
H: x \in xs
size [seq y <- a :: xs | P y] =
size [seq y <- rem (T:=X) x (a :: xs) | P y] + 1
    {
X: eqType
x: X
P: pred X
H0: P x
a: X
xs: seq X
IHxs: x \in xs ->
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
H: x \in xs
size [seq y <- a :: xs | P y] =
size [seq y <- rem (T:=X) x (a :: xs) | P y] + 1 specialize (IHxs H); simpl in *.
X: eqType
x: X
P: pred X
H0: P x
a: X
xs: seq X
IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
H: x \in xs
size
  (if P a
   then a :: [seq y <- xs | P y]
   else [seq y <- xs | P y]) =
size
  [seq y <- if a == x
            then xs
            else a :: rem (T:=X) x xs
     | P y] + 1
      case EQab: (a == x); simpl.
X: eqType
x: X
P: pred X
H0: P x
a: X
xs: seq X
IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
H: x \in xs
EQab: (a == x) = true
size
  (if P a
   then a :: [seq y <- xs | P y]
   else [seq y <- xs | P y]) =
size [seq y <- xs | P y] + 1
X: eqType
x: X
P: pred X
H0: P x
a: X
xs: seq X
IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
H: x \in xs
EQab: (a == x) = false
size
  (if P a
   then a :: [seq y <- xs | P y]
   else [seq y <- xs | P y]) =
size
  (if P a
   then a :: [seq y <- rem (T:=X) x xs | P y]
   else [seq y <- rem (T:=X) x xs | P y]) + 1
      {
X: eqType
x: X
P: pred X
H0: P x
a: X
xs: seq X
IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
H: x \in xs
EQab: (a == x) = true
size
  (if P a
   then a :: [seq y <- xs | P y]
   else [seq y <- xs | P y]) =
size [seq y <- xs | P y] + 1 move: EQab => /eqP EQab; subst.
X: eqType
x: X
P: pred X
H0: P x
xs: seq X
IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
H: x \in xs
size
  (if P x
   then x :: [seq y <- xs | P y]
   else [seq y <- xs | P y]) =
size [seq y <- xs | P y] + 1
        by rewrite H0 addn1. }
X: eqType
x: X
P: pred X
H0: P x
a: X
xs: seq X
IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
H: x \in xs
EQab: (a == x) = false
size
  (if P a
   then a :: [seq y <- xs | P y]
   else [seq y <- xs | P y]) =
size
  (if P a
   then a :: [seq y <- rem (T:=X) x xs | P y]
   else [seq y <- rem (T:=X) x xs | P y]) + 1
      {
X: eqType
x: X
P: pred X
H0: P x
a: X
xs: seq X
IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
H: x \in xs
EQab: (a == x) = false
size
  (if P a
   then a :: [seq y <- xs | P y]
   else [seq y <- xs | P y]) =
size
  (if P a
   then a :: [seq y <- rem (T:=X) x xs | P y]
   else [seq y <- rem (T:=X) x xs | P y]) + 1 case Pa: (P a); simpl.
X: eqType
x: X
P: pred X
H0: P x
a: X
xs: seq X
IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
H: x \in xs
EQab: (a == x) = false
Pa: P a = true
(size [seq y <- xs | P y]).+1 =
(size [seq y <- rem (T:=X) x xs | P y]).+1 + 1
X: eqType
x: X
P: pred X
H0: P x
a: X
xs: seq X
IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
H: x \in xs
EQab: (a == x) = false
Pa: P a = false
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
        -
X: eqType
x: X
P: pred X
H0: P x
a: X
xs: seq X
IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
H: x \in xs
EQab: (a == x) = false
Pa: P a = true
(size [seq y <- xs | P y]).+1 =
(size [seq y <- rem (T:=X) x xs | P y]).+1 + 1 by rewrite IHxs !addn1.
        -
X: eqType
x: X
P: pred X
H0: P x
a: X
xs: seq X
IHxs: size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1
H: x \in xs
EQab: (a == x) = false
Pa: P a = false
size [seq y <- xs | P y] =
size [seq y <- rem (T:=X) x xs | P y] + 1 by rewrite IHxs.
      }
    }
  Qed.

End RemList.

(** Additional lemmas about sequences. *)
Section AdditionalLemmas.

  (** First, we show that a sequence [xs] contains the same elements
      as a sequence [undup xs]. *)
  Lemma in_seq_equiv_undup :
    forall {X : eqType} (xs : seq X) (x : X),
      (x \in undup xs) = (x \in xs).
forall (X : eqType) (xs : seq X) (x : X),
(x \in undup xs) = (x \in xs)
  Proof.
forall (X : eqType) (xs : seq X) (x : X),
(x \in undup xs) = (x \in xs)
    move=> X xs; induction xs as [ | x0 xs IHxs]; first by done.
X: eqType
x0: X
xs: seq X
IHxs: forall x : X, (x \in undup xs) = (x \in xs)
forall x : X,
(x \in undup (x0 :: xs)) = (x \in x0 :: xs)
    move=> x; rewrite in_cons //=; case IN: (x0 \in xs).
X: eqType
x0: X
xs: seq X
IHxs: forall x : X, (x \in undup xs) = (x \in xs)
x: X
IN: (x0 \in xs) = true
(x \in undup xs) = (x == x0) || (x \in xs)
X: eqType
x0: X
xs: seq X
IHxs: forall x : X, (x \in undup xs) = (x \in xs)
x: X
IN: (x0 \in xs) = false
(x \in x0 :: undup xs) = (x == x0) || (x \in xs)
    -
X: eqType
x0: X
xs: seq X
IHxs: forall x : X, (x \in undup xs) = (x \in xs)
x: X
IN: (x0 \in xs) = true
(x \in undup xs) = (x == x0) || (x \in xs) case EQ: (x == x0).
X: eqType
x0: X
xs: seq X
IHxs: forall x : X, (x \in undup xs) = (x \in xs)
x: X
IN: (x0 \in xs) = true
EQ: (x == x0) = true
(x \in undup xs) = true || (x \in xs)
X: eqType
x0: X
xs: seq X
IHxs: forall x : X, (x \in undup xs) = (x \in xs)
x: X
IN: (x0 \in xs) = true
EQ: (x == x0) = false
(x \in undup xs) = false || (x \in xs)
      +
X: eqType
x0: X
xs: seq X
IHxs: forall x : X, (x \in undup xs) = (x \in xs)
x: X
IN: (x0 \in xs) = true
EQ: (x == x0) = true
(x \in undup xs) = true || (x \in xs) by move: EQ => /eqP EQ; subst; rewrite orTb IHxs.
      +
X: eqType
x0: X
xs: seq X
IHxs: forall x : X, (x \in undup xs) = (x \in xs)
x: X
IN: (x0 \in xs) = true
EQ: (x == x0) = false
(x \in undup xs) = false || (x \in xs) by rewrite orFb; apply IHxs.
    -
X: eqType
x0: X
xs: seq X
IHxs: forall x : X, (x \in undup xs) = (x \in xs)
x: X
IN: (x0 \in xs) = false
(x \in x0 :: undup xs) = (x == x0) || (x \in xs) by rewrite in_cons IHxs.
  Qed.

  (** We prove that [x::xs = ys] is a sufficient condition for [x] to
      be in [ys]. *)
  Lemma mem_head_impl :
    forall {X : eqType} (x : X) (xs ys : seq X),
      x::xs = ys ->
      x \in ys.
forall (X : eqType) (x : X) (xs ys : seq X),
x :: xs = ys -> x \in ys
  Proof.
forall (X : eqType) (x : X) (xs ys : seq X),
x :: xs = ys -> x \in ys
    intros X x xs [ |y ys] EQ; first by done.
X: eqType
x: X
xs: seq X
y: X
ys: seq X
EQ: x :: xs = y :: ys
x \in y :: ys
    move: EQ => /eqP; rewrite eqseq_cons => /andP [/eqP EQ _].
X: eqType
x: X
xs: seq X
y: X
ys: seq X
EQ: x = y
x \in y :: ys
    by subst y; rewrite in_cons; apply/orP; left.
  Qed.

  (** We show that if [n > 0], then [nth (x::xs) n = nth xs (n-1)]. *)
  Lemma nth0_cons :
    forall x xs n,
      n > 0 ->
      nth 0 (x :: xs) n = nth 0 xs n.-1.
forall (x : nat) (xs : seq nat) (n : nat),
0 < n -> nth 0 (x :: xs) n = nth 0 xs n.-1
  Proof.
forall (x : nat) (xs : seq nat) (n : nat),
0 < n -> nth 0 (x :: xs) n = nth 0 xs n.-1 by move=> ? ? []. Qed.

  (** Equality of singleton lists is identical to equality of option types. *)
  Lemma seq1_some {T : eqType} :
    forall (x y : T),
      ([:: x] == [:: y]) = (Some x == Some y).
T: eqType
forall x y : T,
([:: x] == [:: y]) = (Some x == Some y)
  Proof.
T: eqType
forall x y : T,
([:: x] == [:: y]) = (Some x == Some y)
    move=> x y.
T: eqType
x, y: T
([:: x] == [:: y]) = (Some x == Some y)
    case: (eqVneq x y) => [-> //=|/eqP NEQ]; first by rewrite !eq_refl.
T: eqType
x, y: T
NEQ: x <> y
([:: x] == [:: y]) = (Some x == Some y)
    apply/eqP; rewrite ifF.
T: eqType
x, y: T
NEQ: x <> y
[:: x] <> [:: y]
T: eqType
x, y: T
NEQ: x <> y
(Some x == Some y) = false
    -
T: eqType
x, y: T
NEQ: x <> y
[:: x] <> [:: y] by move=> []EQ; apply: NEQ.
    -
T: eqType
x, y: T
NEQ: x <> y
(Some x == Some y) = false by apply/negbTE/eqP => -[].
  Qed.

  (** We prove that a sequence [xs] of size [n.+1] can be destructed
     into a sequence [xs_l] of size [n] and an element [x] such that
     [x = xs ++ [::x]]. *)
  Lemma seq_elim_last :
    forall {X : Type} (n : nat) (xs : seq X),
      size xs = n.+1 ->
      exists x xs__c, xs = xs__c ++ [:: x] /\ size xs__c = n.
forall (X : Type) (n : nat) (xs : seq X),
size xs = n.+1 ->
exists (x : X) (xs__c : seq X),
  xs = xs__c ++ [:: x] /\ size xs__c = n
  Proof.
forall (X : Type) (n : nat) (xs : seq X),
size xs = n.+1 ->
exists (x : X) (xs__c : seq X),
  xs = xs__c ++ [:: x] /\ size xs__c = n
    intros X n xs SIZE.
X: Type
n: nat
xs: seq X
SIZE: size xs = n.+1
exists (x : X) (xs__c : seq X),
  xs = xs__c ++ [:: x] /\ size xs__c = n
    elim: n xs SIZE => [|n IHn] xs SIZE.
X: Type
xs: seq X
SIZE: size xs = 1
exists (x : X) (xs__c : seq X),
  xs = xs__c ++ [:: x] /\ size xs__c = 0
X: Type
n: nat
IHn: forall xs : seq X,
size xs = n.+1 ->
exists (x : X) (xs__c : seq X),
  xs = xs__c ++ [:: x] /\ size xs__c = n
xs: seq X
SIZE: size xs = n.+2
exists (x : X) (xs__c : seq X),
  xs = xs__c ++ [:: x] /\ size xs__c = n.+1
    -
X: Type
xs: seq X
SIZE: size xs = 1
exists (x : X) (xs__c : seq X),
  xs = xs__c ++ [:: x] /\ size xs__c = 0 destruct xs as [|x xs]; first by done.
X: Type
x: X
xs: seq X
SIZE: size (x :: xs) = 1
exists (x0 : X) (xs__c : seq X),
  x :: xs = xs__c ++ [:: x0] /\ size xs__c = 0
      destruct xs; last by done.
X: Type
x: X
SIZE: size [:: x] = 1
exists (x0 : X) (xs__c : seq X),
  [:: x] = xs__c ++ [:: x0] /\ size xs__c = 0
      by exists x, [::]; split.
    -
X: Type
n: nat
IHn: forall xs : seq X,
size xs = n.+1 ->
exists (x : X) (xs__c : seq X), xs = xs__c ++ [:: x] /\ size xs__c = n
xs: seq X
SIZE: size xs = n.+2
exists (x : X) (xs__c : seq X),
  xs = xs__c ++ [:: x] /\ size xs__c = n.+1 destruct xs as [|x xs]; first by done.
X: Type
n: nat
IHn: forall xs : seq X,
size xs = n.+1 ->
exists (x : X) (xs__c : seq X), xs = xs__c ++ [:: x] /\ size xs__c = n
x: X
xs: seq X
SIZE: size (x :: xs) = n.+2
exists (x0 : X) (xs__c : seq X),
  x :: xs = xs__c ++ [:: x0] /\ size xs__c = n.+1
      specialize (IHn xs).
X: Type
n: nat
xs: seq X
IHn: size xs = n.+1 ->
exists (x : X) (xs__c : seq X), xs = xs__c ++ [:: x] /\ size xs__c = n
x: X
SIZE: size (x :: xs) = n.+2
exists (x0 : X) (xs__c : seq X),
  x :: xs = xs__c ++ [:: x0] /\ size xs__c = n.+1
      feed IHn; first by simpl in SIZE; apply eq_add_S in SIZE.
X: Type
n: nat
xs: seq X
IHn: exists (x : X) (xs__c : seq X), xs = xs__c ++ [:: x] /\ size xs__c = n
x: X
SIZE: size (x :: xs) = n.+2
exists (x0 : X) (xs__c : seq X),
  x :: xs = xs__c ++ [:: x0] /\ size xs__c = n.+1
      destruct IHn as [x__n [xs__n [EQ__n SIZE__n]]]; subst xs.
X: Type
n: nat
x__n: X
xs__n: seq X
SIZE__n: size xs__n = n
x: X
SIZE: size (x :: xs__n ++ [:: x__n]) = n.+2
exists (x0 : X) (xs__c : seq X),
  x :: xs__n ++ [:: x__n] = xs__c ++ [:: x0] /\
  size xs__c = n.+1
      exists x__n, (x :: xs__n); split; first by done.
X: Type
n: nat
x__n: X
xs__n: seq X
SIZE__n: size xs__n = n
x: X
SIZE: size (x :: xs__n ++ [:: x__n]) = n.+2
size (x :: xs__n) = n.+1
      simpl in SIZE; apply eq_add_S in SIZE.
X: Type
n: nat
x__n: X
xs__n: seq X
SIZE__n: size xs__n = n
x: X
SIZE: size (xs__n ++ [:: x__n]) = n.+1
size (x :: xs__n) = n.+1
      rewrite size_cat //= in SIZE; rewrite addn1 in SIZE; apply eq_add_S in SIZE.
X: Type
n: nat
x__n: X
xs__n: seq X
SIZE__n: size xs__n = n
x: X
SIZE: size xs__n = n
size (x :: xs__n) = n.+1
      by apply eq_S.
  Qed.

  (** Next, we prove that [x ∈ xs] implies that [xs] can be split
     into two parts such that [xs = xsl ++ [::x] ++ [xsr]]. *)
  Lemma in_cat :
    forall {X : eqType} (x : X) (xs : list X),
      x \in xs -> exists xsl xsr, xs = xsl ++ [::x] ++ xsr.
forall (X : eqType) (x : X) (xs : seq X),
x \in xs ->
exists xsl xsr : seq X, xs = xsl ++ [:: x] ++ xsr
  Proof.
forall (X : eqType) (x : X) (xs : seq X),
x \in xs ->
exists xsl xsr : seq X, xs = xsl ++ [:: x] ++ xsr
    move=> X x; elim=> [//|a xs IHxs] SUB.
X: eqType
x, a: X
xs: seq X
IHxs: x \in xs ->
exists xsl xsr : seq X,
  xs = xsl ++ [:: x] ++ xsr
SUB: x \in a :: xs
exists xsl xsr : seq X, a :: xs = xsl ++ [:: x] ++ xsr
    move: SUB; rewrite in_cons; move => /orP [/eqP EQ|IN].
X: eqType
x, a: X
xs: seq X
IHxs: x \in xs ->
exists xsl xsr : seq X,
  xs = xsl ++ [:: x] ++ xsr
EQ: x = a
exists xsl xsr : seq X, a :: xs = xsl ++ [:: x] ++ xsr
X: eqType
x, a: X
xs: seq X
IHxs: x \in xs ->
exists xsl xsr : seq X,
  xs = xsl ++ [:: x] ++ xsr
IN: x \in xs
exists xsl xsr : seq X, a :: xs = xsl ++ [:: x] ++ xsr
    -
X: eqType
x, a: X
xs: seq X
IHxs: x \in xs ->
exists xsl xsr : seq X,
  xs = xsl ++ [:: x] ++ xsr
EQ: x = a
exists xsl xsr : seq X, a :: xs = xsl ++ [:: x] ++ xsr by subst; exists [::], xs.
    -
X: eqType
x, a: X
xs: seq X
IHxs: x \in xs ->
exists xsl xsr : seq X,
  xs = xsl ++ [:: x] ++ xsr
IN: x \in xs
exists xsl xsr : seq X, a :: xs = xsl ++ [:: x] ++ xsr feed IHxs; first by done.
X: eqType
x, a: X
xs: seq X
IHxs: exists xsl xsr : seq X,
  xs = xsl ++ [:: x] ++ xsr
IN: x \in xs
exists xsl xsr : seq X, a :: xs = xsl ++ [:: x] ++ xsr
      clear IN; move: IHxs => [xsl [xsr EQ]].
X: eqType
x, a: X
xs, xsl, xsr: seq X
EQ: xs = xsl ++ [:: x] ++ xsr
exists xsl xsr : seq X, a :: xs = xsl ++ [:: x] ++ xsr
      by subst; exists (a::xsl), xsr.
  Qed.

  (** We prove that for any two sequences [xs] and [ys] the fact that [xs] is a sub-sequence
     of [ys] implies that the size of [xs] is at most the size of [ys]. *)
  Lemma subseq_leq_size :
    forall {X : eqType} (xs ys: seq X),
      uniq xs ->
      (forall x, x \in xs -> x \in ys) ->
      size xs <= size ys.
forall (X : eqType) (xs ys : seq X),
uniq xs ->
(forall x : X, x \in xs -> x \in ys) ->
size xs <= size ys
  Proof.
forall (X : eqType) (xs ys : seq X),
uniq xs ->
(forall x : X, x \in xs -> x \in ys) ->
size xs <= size ys
    intros X xs ys UNIQ SUB.
X: eqType
xs, ys: seq X
UNIQ: uniq xs
SUB: forall x : X, x \in xs -> x \in ys
size xs <= size ys
    have EXm: exists m, size ys <= m; first by exists (size ys).
X: eqType
xs, ys: seq X
UNIQ: uniq xs
SUB: forall x : X, x \in xs -> x \in ys
EXm: exists m : nat, size ys <= m
size xs <= size ys
    move: EXm => [m SIZEm].
X: eqType
xs, ys: seq X
UNIQ: uniq xs
SUB: forall x : X, x \in xs -> x \in ys
m: nat
SIZEm: size ys <= m
size xs <= size ys
    move: xs ys SIZEm UNIQ SUB.
X: eqType
m: nat
forall xs ys : seq X,
size ys <= m ->
uniq xs ->
(forall x : X, x \in xs -> x \in ys) ->
size xs <= size ys
    elim: m => [|m IHm] xs ys SIZEm UNIQ SUB.
X: eqType
xs, ys: seq X
SIZEm: size ys <= 0
UNIQ: uniq xs
SUB: forall x : X, x \in xs -> x \in ys
size xs <= size ys
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs ->
(forall x : X, x \in xs -> x \in ys) ->
size xs <= size ys
xs, ys: seq X
SIZEm: size ys <= m.+1
UNIQ: uniq xs
SUB: forall x : X, x \in xs -> x \in ys
size xs <= size ys
    {
X: eqType
xs, ys: seq X
SIZEm: size ys <= 0
UNIQ: uniq xs
SUB: forall x : X, x \in xs -> x \in ys
size xs <= size ys move: SIZEm; rewrite leqn0 size_eq0; move => /eqP SIZEm; subst ys.
X: eqType
xs: seq X
UNIQ: uniq xs
SUB: forall x : X, x \in xs -> x \in [::]
size xs <= size [::]
      destruct xs as [|s xs]; first by done.
X: eqType
s: X
xs: seq X
UNIQ: uniq (s :: xs)
SUB: forall x : X, x \in s :: xs -> x \in [::]
size (s :: xs) <= size [::]
      specialize (SUB s).
X: eqType
s: X
xs: seq X
UNIQ: uniq (s :: xs)
SUB: s \in s :: xs -> s \in [::]
size (s :: xs) <= size [::]
      by feed SUB; [rewrite in_cons; apply/orP; left | done].
    }
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
xs, ys: seq X
SIZEm: size ys <= m.+1
UNIQ: uniq xs
SUB: forall x : X, x \in xs -> x \in ys
size xs <= size ys
    {
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
xs, ys: seq X
SIZEm: size ys <= m.+1
UNIQ: uniq xs
SUB: forall x : X, x \in xs -> x \in ys
size xs <= size ys destruct xs as [ | x xs]; first by done.
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ys: seq X
SIZEm: size ys <= m.+1
UNIQ: uniq (x :: xs)
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
size (x :: xs) <= size ys
      move: (@in_cat _ x ys) => Lem.
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ys: seq X
SIZEm: size ys <= m.+1
UNIQ: uniq (x :: xs)
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
Lem: x \in ys ->
exists xsl xsr : seq X,
  ys = xsl ++ [:: x] ++ xsr
size (x :: xs) <= size ys
      feed Lem; first by apply SUB; rewrite in_cons; apply/orP; left.
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ys: seq X
SIZEm: size ys <= m.+1
UNIQ: uniq (x :: xs)
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
Lem: exists xsl xsr : seq X,
  ys = xsl ++ [:: x] ++ xsr
size (x :: xs) <= size ys
      move: Lem => [ysl [ysr EQ]]; subst ys.
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
SUB: forall x0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
size (x :: xs) <= size (ysl ++ [:: x] ++ ysr)
      rewrite !size_cat //= -addnC add1n addSn ltnS -size_cat; eapply IHm.
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
SUB: forall x0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
size (ysr ++ ysl) <= m
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs ->
(forall x : X, x \in xs -> x \in ys) ->
size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
SUB: forall x0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
uniq xs
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs ->
(forall x : X, x \in xs -> x \in ys) ->
size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
SUB: forall x0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
forall x : X, x \in xs -> x \in ysr ++ ysl
      -
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
SUB: forall x0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
size (ysr ++ ysl) <= m move: SIZEm; rewrite !size_cat //= => SIZE.
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ysl, ysr: seq X
UNIQ: uniq (x :: xs)
SUB: forall x0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
SIZE: size ysl + (1 + size ysr) <= m.+1
size ysr + size ysl <= m
        by rewrite add1n addnS ltnS addnC in SIZE.
      -
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
SUB: forall x0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
uniq xs by move: UNIQ; rewrite cons_uniq => /andP [_ UNIQ].
      -
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
SUB: forall x0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
forall x : X, x \in xs -> x \in ysr ++ ysl intros a IN.
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
SUB: forall x0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
a: X
IN: a \in xs
a \in ysr ++ ysl
        destruct (a == x) eqn: EQ.
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
SUB: forall x0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
a: X
IN: a \in xs
EQ: (a == x) = true
a \in ysr ++ ysl
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs ->
(forall x : X, x \in xs -> x \in ys) ->
size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
SUB: forall x0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
a: X
IN: a \in xs
EQ: (a == x) = false
a \in ysr ++ ysl
        {
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
SUB: forall x0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
a: X
IN: a \in xs
EQ: (a == x) = true
a \in ysr ++ ysl exfalso.
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
SUB: forall x0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
a: X
IN: a \in xs
EQ: (a == x) = true
False
          move: EQ UNIQ; rewrite cons_uniq; move => /eqP EQ /andP [NIN UNIQ].
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
SUB: forall x0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
a: X
IN: a \in xs
EQ: a = x
NIN: x \notin xs
UNIQ: uniq xs
False
          by subst; move: NIN => /negP NIN; apply: NIN.
        }
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
SUB: forall x0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
a: X
IN: a \in xs
EQ: (a == x) = false
a \in ysr ++ ysl
        {
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
SUB: forall x0 : X,
x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
a: X
IN: a \in xs
EQ: (a == x) = false
a \in ysr ++ ysl specialize (SUB a).
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
a: X
SUB: a \in x :: xs -> a \in ysl ++ [:: x] ++ ysr
IN: a \in xs
EQ: (a == x) = false
a \in ysr ++ ysl
          feed SUB; first by rewrite in_cons; apply/orP; right.
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
a: X
SUB: a \in ysl ++ [:: x] ++ ysr
IN: a \in xs
EQ: (a == x) = false
a \in ysr ++ ysl
          clear IN; move: SUB; rewrite !mem_cat; move => /orP [IN| /orP [IN|IN]].
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
a: X
EQ: (a == x) = false
IN: a \in ysl
(a \in ysr) || (a \in ysl)
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs ->
(forall x : X, x \in xs -> x \in ys) ->
size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
a: X
EQ: (a == x) = false
IN: a \in [:: x]
(a \in ysr) || (a \in ysl)
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs ->
(forall x : X, x \in xs -> x \in ys) ->
size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
a: X
EQ: (a == x) = false
IN: a \in ysr
(a \in ysr) || (a \in ysl)
          -
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
a: X
EQ: (a == x) = false
IN: a \in ysl
(a \in ysr) || (a \in ysl) by apply/orP; right.
          -
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
a: X
EQ: (a == x) = false
IN: a \in [:: x]
(a \in ysr) || (a \in ysl) by exfalso; move: IN; rewrite in_cons => /orP [IN|IN]; [rewrite IN in EQ | ].
          -
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
x: X
xs, ysl, ysr: seq X
SIZEm: size (ysl ++ [:: x] ++ ysr) <= m.+1
UNIQ: uniq (x :: xs)
a: X
EQ: (a == x) = false
IN: a \in ysr
(a \in ysr) || (a \in ysl) by apply/orP; left.
        }
    }
  Qed.

  (** Given two sequences [xs] and [ys], two elements [x] and [y], and
      an index [idx] such that [nth xs idx = x, nth ys idx = y], we
      show that the pair [(x, y)] is in [zip xs ys]. *)
  Lemma in_zip :
    forall {X Y : eqType} (xs : seq X) (ys : seq Y) (x x__d : X) (y y__d : Y),
      size xs = size ys ->
      (exists idx, idx < size xs /\ nth x__d xs idx = x /\ nth y__d ys idx = y) ->
      (x, y) \in zip xs ys.
forall (X Y : eqType) (xs : seq X) (ys : seq Y)
  (x x__d : X) (y y__d : Y),
size xs = size ys ->
(exists idx : nat,
   idx < size xs /\
   nth x__d xs idx = x /\ nth y__d ys idx = y) ->
(x, y) \in zip xs ys
  Proof.
forall (X Y : eqType) (xs : seq X) (ys : seq Y)
  (x x__d : X) (y y__d : Y),
size xs = size ys ->
(exists idx : nat,
   idx < size xs /\
   nth x__d xs idx = x /\ nth y__d ys idx = y) ->
(x, y) \in zip xs ys
    move=> X Y xs ys x x__d y y__d.
X, Y: eqType
xs: seq X
ys: seq Y
x, x__d: X
y, y__d: Y
size xs = size ys ->
(exists idx : nat,
   idx < size xs /\
   nth x__d xs idx = x /\ nth y__d ys idx = y) ->
(x, y) \in zip xs ys
    elim: xs ys => [|x1 xs IHxs] ys EQ [idx [LT [NTHx NTHy]]] //.
X, Y: eqType
x, x__d: X
y, y__d: Y
x1: X
xs: seq X
IHxs: forall ys : seq Y,
size xs = size ys ->
(exists idx : nat,
   idx < size xs /\
   nth x__d xs idx = x /\ nth y__d ys idx = y) ->
(x, y) \in zip xs ys
ys: seq Y
EQ: size (x1 :: xs) = size ys
idx: nat
LT: idx < size (x1 :: xs)
NTHx: nth x__d (x1 :: xs) idx = x
NTHy: nth y__d ys idx = y
(x, y) \in zip (x1 :: xs) ys
    destruct ys as [ | y1 ys]; first by done.
X, Y: eqType
x, x__d: X
y, y__d: Y
x1: X
xs: seq X
IHxs: forall ys : seq Y,
size xs = size ys ->
(exists idx : nat,
   idx < size xs /\
   nth x__d xs idx = x /\ nth y__d ys idx = y) ->
(x, y) \in zip xs ys
y1: Y
ys: seq Y
EQ: size (x1 :: xs) = size (y1 :: ys)
idx: nat
LT: idx < size (x1 :: xs)
NTHx: nth x__d (x1 :: xs) idx = x
NTHy: nth y__d (y1 :: ys) idx = y
(x, y) \in zip (x1 :: xs) (y1 :: ys)
    rewrite //= in_cons; apply/orP.
X, Y: eqType
x, x__d: X
y, y__d: Y
x1: X
xs: seq X
IHxs: forall ys : seq Y,
size xs = size ys ->
(exists idx : nat,
   idx < size xs /\
   nth x__d xs idx = x /\ nth y__d ys idx = y) ->
(x, y) \in zip xs ys
y1: Y
ys: seq Y
EQ: size (x1 :: xs) = size (y1 :: ys)
idx: nat
LT: idx < size (x1 :: xs)
NTHx: nth x__d (x1 :: xs) idx = x
NTHy: nth y__d (y1 :: ys) idx = y
(x, y) == (x1, y1) \/ (x, y) \in zip xs ys
    destruct idx as [ | idx]; [left | right].
X, Y: eqType
x, x__d: X
y, y__d: Y
x1: X
xs: seq X
IHxs: forall ys : seq Y,
size xs = size ys ->
(exists idx : nat,
   idx < size xs /\
   nth x__d xs idx = x /\ nth y__d ys idx = y) ->
(x, y) \in zip xs ys
y1: Y
ys: seq Y
EQ: size (x1 :: xs) = size (y1 :: ys)
LT: 0 < size (x1 :: xs)
NTHx: nth x__d (x1 :: xs) 0 = x
NTHy: nth y__d (y1 :: ys) 0 = y
(x, y) == (x1, y1)
X, Y: eqType
x, x__d: X
y, y__d: Y
x1: X
xs: seq X
IHxs: forall ys : seq Y,
size xs = size ys ->
(exists idx : nat,
   idx < size xs /\
   nth x__d xs idx = x /\ nth y__d ys idx = y) ->
(x, y) \in zip xs ys
y1: Y
ys: seq Y
EQ: size (x1 :: xs) = size (y1 :: ys)
idx: nat
LT: idx.+1 < size (x1 :: xs)
NTHx: nth x__d (x1 :: xs) idx.+1 = x
NTHy: nth y__d (y1 :: ys) idx.+1 = y
(x, y) \in zip xs ys
    {
X, Y: eqType
x, x__d: X
y, y__d: Y
x1: X
xs: seq X
IHxs: forall ys : seq Y,
size xs = size ys ->
(exists idx : nat,
   idx < size xs /\
   nth x__d xs idx = x /\ nth y__d ys idx = y) ->
(x, y) \in zip xs ys
y1: Y
ys: seq Y
EQ: size (x1 :: xs) = size (y1 :: ys)
LT: 0 < size (x1 :: xs)
NTHx: nth x__d (x1 :: xs) 0 = x
NTHy: nth y__d (y1 :: ys) 0 = y
(x, y) == (x1, y1) by simpl in NTHx, NTHy; subst. }
X, Y: eqType
x, x__d: X
y, y__d: Y
x1: X
xs: seq X
IHxs: forall ys : seq Y,
size xs = size ys ->
(exists idx : nat,
   idx < size xs /\
   nth x__d xs idx = x /\ nth y__d ys idx = y) ->
(x, y) \in zip xs ys
y1: Y
ys: seq Y
EQ: size (x1 :: xs) = size (y1 :: ys)
idx: nat
LT: idx.+1 < size (x1 :: xs)
NTHx: nth x__d (x1 :: xs) idx.+1 = x
NTHy: nth y__d (y1 :: ys) idx.+1 = y
(x, y) \in zip xs ys
    {
X, Y: eqType
x, x__d: X
y, y__d: Y
x1: X
xs: seq X
IHxs: forall ys : seq Y,
size xs = size ys ->
(exists idx : nat,
   idx < size xs /\
   nth x__d xs idx = x /\ nth y__d ys idx = y) ->
(x, y) \in zip xs ys
y1: Y
ys: seq Y
EQ: size (x1 :: xs) = size (y1 :: ys)
idx: nat
LT: idx.+1 < size (x1 :: xs)
NTHx: nth x__d (x1 :: xs) idx.+1 = x
NTHy: nth y__d (y1 :: ys) idx.+1 = y
(x, y) \in zip xs ys simpl in NTHx, NTHy, LT.
X, Y: eqType
x, x__d: X
y, y__d: Y
x1: X
xs: seq X
IHxs: forall ys : seq Y,
size xs = size ys ->
(exists idx : nat,
   idx < size xs /\
   nth x__d xs idx = x /\ nth y__d ys idx = y) ->
(x, y) \in zip xs ys
y1: Y
ys: seq Y
EQ: size (x1 :: xs) = size (y1 :: ys)
idx: nat
LT: idx.+1 < (size xs).+1
NTHx: nth x__d xs idx = x
NTHy: nth y__d ys idx = y
(x, y) \in zip xs ys
      eapply IHxs.
X, Y: eqType
x, x__d: X
y, y__d: Y
x1: X
xs: seq X
IHxs: forall ys : seq Y,
size xs = size ys ->
(exists idx : nat,
   idx < size xs /\
   nth x__d xs idx = x /\ nth y__d ys idx = y) ->
(x, y) \in zip xs ys
y1: Y
ys: seq Y
EQ: size (x1 :: xs) = size (y1 :: ys)
idx: nat
LT: idx.+1 < (size xs).+1
NTHx: nth x__d xs idx = x
NTHy: nth y__d ys idx = y
size xs = size ys
X, Y: eqType
x, x__d: X
y, y__d: Y
x1: X
xs: seq X
IHxs: forall ys : seq Y,
size xs = size ys ->
(exists idx : nat,
   idx < size xs /\
   nth x__d xs idx = x /\ nth y__d ys idx = y) ->
(x, y) \in zip xs ys
y1: Y
ys: seq Y
EQ: size (x1 :: xs) = size (y1 :: ys)
idx: nat
LT: idx.+1 < (size xs).+1
NTHx: nth x__d xs idx = x
NTHy: nth y__d ys idx = y
exists idx : nat,
  idx < size xs /\
  nth x__d xs idx = x /\ nth y__d ys idx = y
      -
X, Y: eqType
x, x__d: X
y, y__d: Y
x1: X
xs: seq X
IHxs: forall ys : seq Y,
size xs = size ys ->
(exists idx : nat,
   idx < size xs /\
   nth x__d xs idx = x /\ nth y__d ys idx = y) ->
(x, y) \in zip xs ys
y1: Y
ys: seq Y
EQ: size (x1 :: xs) = size (y1 :: ys)
idx: nat
LT: idx.+1 < (size xs).+1
NTHx: nth x__d xs idx = x
NTHy: nth y__d ys idx = y
size xs = size ys by apply eq_add_S.
      -
X, Y: eqType
x, x__d: X
y, y__d: Y
x1: X
xs: seq X
IHxs: forall ys : seq Y,
size xs = size ys ->
(exists idx : nat,
   idx < size xs /\
   nth x__d xs idx = x /\ nth y__d ys idx = y) ->
(x, y) \in zip xs ys
y1: Y
ys: seq Y
EQ: size (x1 :: xs) = size (y1 :: ys)
idx: nat
LT: idx.+1 < (size xs).+1
NTHx: nth x__d xs idx = x
NTHy: nth y__d ys idx = y
exists idx : nat,
  idx < size xs /\
  nth x__d xs idx = x /\ nth y__d ys idx = y by exists idx; repeat split; eauto.
    }
  Qed.

  (** This lemma allows us to check proposition of the form
      [forall x ∈ xs, exists y ∈ ys, P x y] using a boolean expression
      [all P (zip xs ys)]. *)
  Lemma forall_exists_implied_by_forall_in_zip:
    forall {X Y : eqType} (P_bool : X * Y -> bool) (P_prop : X -> Y -> Prop) (xs : seq X),
      (forall x y, P_bool (x, y) <-> P_prop x y) ->
      (exists ys, size xs = size ys /\ all P_bool (zip xs ys) == true) ->
      (forall x, x \in xs -> exists y, P_prop x y).
forall (X Y : eqType) (P_bool : X * Y -> bool)
  (P_prop : X -> Y -> Prop) (xs : seq X),
(forall (x : X) (y : Y), P_bool (x, y) <-> P_prop x y) ->
(exists ys : seq Y,
   size xs = size ys /\ all P_bool (zip xs ys) == true) ->
forall x : X, x \in xs -> exists y : Y, P_prop x y
  Proof.
forall (X Y : eqType) (P_bool : X * Y -> bool)
  (P_prop : X -> Y -> Prop) (xs : seq X),
(forall (x : X) (y : Y), P_bool (x, y) <-> P_prop x y) ->
(exists ys : seq Y,
   size xs = size ys /\ all P_bool (zip xs ys) == true) ->
forall x : X, x \in xs -> exists y : Y, P_prop x y
    move=> X Y P_bool P_prop xs EQ TR x IN.
X, Y: eqType
P_bool: X * Y -> bool
P_prop: X -> Y -> Prop
xs: seq X
EQ: forall (x : X) (y : Y),
P_bool (x, y) <-> P_prop x y
TR: exists ys : seq Y,
  size xs = size ys /\
  all P_bool (zip xs ys) == true
x: X
IN: x \in xs
exists y : Y, P_prop x y
    destruct TR as [ys [SIZE ALL]].
X, Y: eqType
P_bool: X * Y -> bool
P_prop: X -> Y -> Prop
xs: seq X
EQ: forall (x : X) (y : Y),
P_bool (x, y) <-> P_prop x y
ys: seq Y
SIZE: size xs = size ys
ALL: all P_bool (zip xs ys) == true
x: X
IN: x \in xs
exists y : Y, P_prop x y
    set (idx := index x xs).
X, Y: eqType
P_bool: X * Y -> bool
P_prop: X -> Y -> Prop
xs: seq X
EQ: forall (x : X) (y : Y),
P_bool (x, y) <-> P_prop x y
ys: seq Y
SIZE: size xs = size ys
ALL: all P_bool (zip xs ys) == true
x: X
IN: x \in xs
idx:= index x xs: nat
exists y : Y, P_prop x y
    have x__d : Y by destruct xs, ys.
X, Y: eqType
P_bool: X * Y -> bool
P_prop: X -> Y -> Prop
xs: seq X
EQ: forall (x : X) (y : Y),
P_bool (x, y) <-> P_prop x y
ys: seq Y
SIZE: size xs = size ys
ALL: all P_bool (zip xs ys) == true
x: X
IN: x \in xs
idx:= index x xs: nat
x__d: Y
exists y : Y, P_prop x y
    have y__d : Y by destruct xs, ys.
X, Y: eqType
P_bool: X * Y -> bool
P_prop: X -> Y -> Prop
xs: seq X
EQ: forall (x : X) (y : Y),
P_bool (x, y) <-> P_prop x y
ys: seq Y
SIZE: size xs = size ys
ALL: all P_bool (zip xs ys) == true
x: X
IN: x \in xs
idx:= index x xs: nat
x__d, y__d: Y
exists y : Y, P_prop x y
    exists (nth y__d ys idx); apply EQ; clear EQ.
X, Y: eqType
P_bool: X * Y -> bool
P_prop: X -> Y -> Prop
xs: seq X
ys: seq Y
SIZE: size xs = size ys
ALL: all P_bool (zip xs ys) == true
x: X
IN: x \in xs
idx:= index x xs: nat
x__d, y__d: Y
P_bool (x, nth y__d ys idx)
    move: ALL => /eqP/allP -> //.
X, Y: eqType
P_bool: X * Y -> bool
P_prop: X -> Y -> Prop
xs: seq X
ys: seq Y
SIZE: size xs = size ys
x: X
IN: x \in xs
idx:= index x xs: nat
x__d, y__d: Y
(x, nth y__d ys idx) \in zip xs ys
    eapply in_zip; first by done.
X, Y: eqType
P_bool: X * Y -> bool
P_prop: X -> Y -> Prop
xs: seq X
ys: seq Y
SIZE: size xs = size ys
x: X
IN: x \in xs
idx:= index x xs: nat
x__d, y__d: Y
exists idx0 : nat,
  idx0 < size xs /\
  nth ?x__d xs idx0 = x /\
  nth ?y__d ys idx0 = nth y__d ys idx
    exists idx; repeat split.
X, Y: eqType
P_bool: X * Y -> bool
P_prop: X -> Y -> Prop
xs: seq X
ys: seq Y
SIZE: size xs = size ys
x: X
IN: x \in xs
idx:= index x xs: nat
x__d, y__d: Y
idx < size xs
X, Y: eqType
P_bool: X * Y -> bool
P_prop: X -> Y -> Prop
xs: seq X
ys: seq Y
SIZE: size xs = size ys
x: X
IN: x \in xs
idx:= index x xs: nat
x__d, y__d: Y
nth ?x__d xs idx = x
    -
X, Y: eqType
P_bool: X * Y -> bool
P_prop: X -> Y -> Prop
xs: seq X
ys: seq Y
SIZE: size xs = size ys
x: X
IN: x \in xs
idx:= index x xs: nat
x__d, y__d: Y
idx < size xs by rewrite index_mem.
    -
X, Y: eqType
P_bool: X * Y -> bool
P_prop: X -> Y -> Prop
xs: seq X
ys: seq Y
SIZE: size xs = size ys
x: X
IN: x \in xs
idx:= index x xs: nat
x__d, y__d: Y
nth ?x__d xs idx = x by apply nth_index.
      Unshelve.
X, Y: eqType
P_bool: X * Y -> bool
P_prop: X -> Y -> Prop
xs: seq X
ys: seq Y
SIZE: size xs = size ys
x: X
IN: x \in xs
idx:= index x xs: nat
x__d, y__d: Y
X by done.
  Qed.

  (** Given two sequences [xs] and [ys] of equal size and without
      duplicates, the fact that [xs ⊆ ys] implies that [ys ⊆ xs]. *)
  Lemma subseq_eq:
    forall {X : eqType} (xs ys : seq X),
      uniq xs ->
      uniq ys ->
      size xs = size ys ->
      (forall x, x \in xs -> x \in ys) ->
      (forall x, x \in ys -> x \in xs).
forall (X : eqType) (xs ys : seq X),
uniq xs ->
uniq ys ->
size xs = size ys ->
(forall x : X, x \in xs -> x \in ys) ->
forall x : X, x \in ys -> x \in xs
  Proof.
forall (X : eqType) (xs ys : seq X),
uniq xs ->
uniq ys ->
size xs = size ys ->
(forall x : X, x \in xs -> x \in ys) ->
forall x : X, x \in ys -> x \in xs
    intros X xs ys UNIQ SUB.
X: eqType
xs, ys: seq X
UNIQ: uniq xs
SUB: uniq ys
size xs = size ys ->
(forall x : X, x \in xs -> x \in ys) ->
forall x : X, x \in ys -> x \in xs
    have EXm: exists m, size ys <= m; first by exists (size ys).
X: eqType
xs, ys: seq X
UNIQ: uniq xs
SUB: uniq ys
EXm: exists m : nat, size ys <= m
size xs = size ys ->
(forall x : X, x \in xs -> x \in ys) ->
forall x : X, x \in ys -> x \in xs
    move: EXm => [m SIZEm].
X: eqType
xs, ys: seq X
UNIQ: uniq xs
SUB: uniq ys
m: nat
SIZEm: size ys <= m
size xs = size ys ->
(forall x : X, x \in xs -> x \in ys) ->
forall x : X, x \in ys -> x \in xs
    move: SIZEm UNIQ SUB; move: xs ys.
X: eqType
m: nat
forall xs ys : seq X,
size ys <= m ->
uniq xs ->
uniq ys ->
size xs = size ys ->
(forall x : X, x \in xs -> x \in ys) ->
forall x : X, x \in ys -> x \in xs
    elim: m => [|m IHm] xs ys SIZEm UNIQx UNIQy EQ SUB a IN.
X: eqType
xs, ys: seq X
SIZEm: size ys <= 0
UNIQx: uniq xs
UNIQy: uniq ys
EQ: size xs = size ys
SUB: forall x : X, x \in xs -> x \in ys
a: X
IN: a \in ys
a \in xs
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs ->
uniq ys ->
size xs = size ys ->
(forall x : X, x \in xs -> x \in ys) ->
forall x : X, x \in ys -> x \in xs
xs, ys: seq X
SIZEm: size ys <= m.+1
UNIQx: uniq xs
UNIQy: uniq ys
EQ: size xs = size ys
SUB: forall x : X, x \in xs -> x \in ys
a: X
IN: a \in ys
a \in xs
    {
X: eqType
xs, ys: seq X
SIZEm: size ys <= 0
UNIQx: uniq xs
UNIQy: uniq ys
EQ: size xs = size ys
SUB: forall x : X, x \in xs -> x \in ys
a: X
IN: a \in ys
a \in xs by move: SIZEm; rewrite leqn0 size_eq0; move => /eqP SIZEm; subst ys. }
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs ->
uniq ys ->
size xs = size ys ->
(forall x : X, x \in xs -> x \in ys) -> forall x : X, x \in ys -> x \in xs
xs, ys: seq X
SIZEm: size ys <= m.+1
UNIQx: uniq xs
UNIQy: uniq ys
EQ: size xs = size ys
SUB: forall x : X, x \in xs -> x \in ys
a: X
IN: a \in ys
a \in xs
    {
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs ->
uniq ys ->
size xs = size ys ->
(forall x : X, x \in xs -> x \in ys) -> forall x : X, x \in ys -> x \in xs
xs, ys: seq X
SIZEm: size ys <= m.+1
UNIQx: uniq xs
UNIQy: uniq ys
EQ: size xs = size ys
SUB: forall x : X, x \in xs -> x \in ys
a: X
IN: a \in ys
a \in xs destruct xs as [ | x xs].
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs ->
uniq ys ->
size xs = size ys ->
(forall x : X, x \in xs -> x \in ys) -> forall x : X, x \in ys -> x \in xs
ys: seq X
SIZEm: size ys <= m.+1
UNIQx: uniq [::]
UNIQy: uniq ys
EQ: size [::] = size ys
SUB: forall x : X, x \in [::] -> x \in ys
a: X
IN: a \in ys
a \in [::]
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs ->
uniq ys ->
size xs = size ys ->
(forall x : X, x \in xs -> x \in ys) ->
forall x : X, x \in ys -> x \in xs
x: X
xs, ys: seq X
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
a \in x :: xs
      {
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs ->
uniq ys ->
size xs = size ys ->
(forall x : X, x \in xs -> x \in ys) -> forall x : X, x \in ys -> x \in xs
ys: seq X
SIZEm: size ys <= m.+1
UNIQx: uniq [::]
UNIQy: uniq ys
EQ: size [::] = size ys
SUB: forall x : X, x \in [::] -> x \in ys
a: X
IN: a \in ys
a \in [::] by move: EQ; simpl => /eqP; rewrite eq_sym size_eq0 => /eqP EQ; subst ys. }
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs ->
uniq ys ->
size xs = size ys ->
(forall x : X, x \in xs -> x \in ys) -> forall x : X, x \in ys -> x \in xs
x: X
xs, ys: seq X
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
a \in x :: xs
      {
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs ->
uniq ys ->
size xs = size ys ->
(forall x : X, x \in xs -> x \in ys) -> forall x : X, x \in ys -> x \in xs
x: X
xs, ys: seq X
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
a \in x :: xs destruct (x == a) eqn:XA; first by rewrite in_cons eq_sym; apply/orP; left.
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs ->
uniq ys ->
size xs = size ys ->
(forall x : X, x \in xs -> x \in ys) -> forall x : X, x \in ys -> x \in xs
x: X
xs, ys: seq X
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
XA: (x == a) = false
a \in x :: xs
        move: XA => /negP/negP NEQ.
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs ->
uniq ys ->
size xs = size ys ->
(forall x : X, x \in xs -> x \in ys) -> forall x : X, x \in ys -> x \in xs
x: X
xs, ys: seq X
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
a \in x :: xs
        rewrite in_cons eq_sym; apply/orP; right.
X: eqType
m: nat
IHm: forall xs ys : seq X,
size ys <= m ->
uniq xs ->
uniq ys ->
size xs = size ys ->
(forall x : X, x \in xs -> x \in ys) -> forall x : X, x \in ys -> x \in xs
x: X
xs, ys: seq X
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
a \in xs
        specialize (IHm xs (rem x ys)); apply IHm.
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
size (rem (T:=X) x ys) <= m
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X,
 x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
uniq xs
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X,
 x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
uniq (rem (T:=X) x ys)
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X,
 x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
size xs = size (rem (T:=X) x ys)
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X,
 x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X,
 x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
a \in rem (T:=X) x ys
        {
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
size (rem (T:=X) x ys) <= m rewrite size_rem; last by apply SUB; rewrite in_cons; apply/orP; left.
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
(size ys).-1 <= m
          by rewrite -EQ //=; move: SIZEm; rewrite -EQ //=. }
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
uniq xs
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X,
 x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
uniq (rem (T:=X) x ys)
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X,
 x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
size xs = size (rem (T:=X) x ys)
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X,
 x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X,
 x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
a \in rem (T:=X) x ys
        {
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
uniq xs by move: UNIQx; rewrite cons_uniq => /andP [_ UNIQ]. }
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
uniq (rem (T:=X) x ys)
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X,
 x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
size xs = size (rem (T:=X) x ys)
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X,
 x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X,
 x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
a \in rem (T:=X) x ys
        {
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
uniq (rem (T:=X) x ys) by apply rem_uniq. }
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
size xs = size (rem (T:=X) x ys)
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X,
 x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X,
 x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
a \in rem (T:=X) x ys
        {
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
size xs = size (rem (T:=X) x ys) rewrite size_rem; last by apply SUB; rewrite in_cons; apply/orP; left.
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
size xs = (size ys).-1
          by rewrite -EQ //=. }
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X,
 x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
a \in rem (T:=X) x ys
        {
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys intros b INb.
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
b: X
INb: b \in xs
b \in rem (T:=X) x ys
          apply in_neq_impl_rem_in.
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
b: X
INb: b \in xs
b \in ys
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X,
 x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X,
x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
b: X
INb: b \in xs
b != x
          -
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
b: X
INb: b \in xs
b \in ys  apply SUB.
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
b: X
INb: b \in xs
b \in x :: xs
             rewrite in_cons.
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
b: X
INb: b \in xs
(b == x) || (b \in xs)
             by apply/orP; right.
          -
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
b: X
INb: b \in xs
b != x move: UNIQx.
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
b: X
INb: b \in xs
uniq (x :: xs) -> b != x
            rewrite cons_uniq => /andP [NIN _].
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
b: X
INb: b \in xs
NIN: x \notin xs
b != x
            apply/negP => /eqP EQbx; subst.
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
INb: x \in xs
NIN: x \notin xs
False
            by move: NIN => /negP NIN; apply: NIN.
        }
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
a \in rem (T:=X) x ys
        {
X: eqType
m: nat
x: X
xs, ys: seq X
IHm: size (rem (T:=X) x ys) <= m ->
uniq xs ->
uniq (rem (T:=X) x ys) ->
size xs = size (rem (T:=X) x ys) ->
(forall x0 : X, x0 \in xs -> x0 \in rem (T:=X) x ys) ->
forall x0 : X, x0 \in rem (T:=X) x ys -> x0 \in xs
SIZEm: size ys <= m.+1
UNIQx: uniq (x :: xs)
UNIQy: uniq ys
EQ: size (x :: xs) = size ys
SUB: forall x0 : X, x0 \in x :: xs -> x0 \in ys
a: X
IN: a \in ys
NEQ: x != a
a \in rem (T:=X) x ys by apply in_neq_impl_rem_in; last rewrite eq_sym. }
      }
    }
  Qed.

  (** We prove that if no element of a sequence [xs] satisfies a
     predicate [P], then [filter P xs] is equal to an empty
     sequence. *)
  Lemma filter_in_pred0 :
    forall {X : eqType} (xs : seq X) (P : pred X),
      (forall x, x \in xs -> ~~ P x) ->
      filter P xs = [::].
forall (X : eqType) (xs : seq X) (P : pred X),
(forall x : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
  Proof.
forall (X : eqType) (xs : seq X) (P : pred X),
(forall x : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
    move=> X xs P; elim: xs => [//|a xs IHxs] ALLF.
X: eqType
P: pred X
a: X
xs: seq X
IHxs: (forall x : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
ALLF: forall x : X, x \in a :: xs -> ~~ P x
[seq x <- a :: xs | P x] = [::]
    rewrite //= IHxs; last first.
X: eqType
P: pred X
a: X
xs: seq X
IHxs: (forall x : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
ALLF: forall x : X, x \in a :: xs -> ~~ P x
forall x : X, x \in xs -> ~~ P x
X: eqType
P: pred X
a: X
xs: seq X
IHxs: (forall x : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
ALLF: forall x : X, x \in a :: xs -> ~~ P x
(if P a then [:: a] else [::]) = [::]
    +
X: eqType
P: pred X
a: X
xs: seq X
IHxs: (forall x : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
ALLF: forall x : X, x \in a :: xs -> ~~ P x
forall x : X, x \in xs -> ~~ P x by intros; apply ALLF; rewrite in_cons; apply/orP; right.
    +
X: eqType
P: pred X
a: X
xs: seq X
IHxs: (forall x : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
ALLF: forall x : X, x \in a :: xs -> ~~ P x
(if P a then [:: a] else [::]) = [::] destruct (P a) eqn:EQ; last by done.
X: eqType
P: pred X
a: X
xs: seq X
IHxs: (forall x : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
ALLF: forall x : X, x \in a :: xs -> ~~ P x
EQ: P a = true
[:: a] = [::]
      move: EQ => /eqP; rewrite eqb_id -[P a]Bool.negb_involutive; move => /negP T.
X: eqType
P: pred X
a: X
xs: seq X
IHxs: (forall x : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
ALLF: forall x : X, x \in a :: xs -> ~~ P x
T: ~ ~~ P a
[:: a] = [::]
      exfalso; apply: T.
X: eqType
P: pred X
a: X
xs: seq X
IHxs: (forall x : X, x \in xs -> ~~ P x) ->
[seq x <- xs | P x] = [::]
ALLF: forall x : X, x \in a :: xs -> ~~ P x
~~ P a
      by apply ALLF; apply/orP; left.
  Qed.

  (** We show that any two elements having the same index in a
      sequence must be equal. *)
  Lemma eq_ind_in_seq :
    forall {X : eqType} (a b : X) (xs : seq X),
      index a xs = index b xs ->
      a \in xs ->
      b \in xs ->
      a = b.
forall (X : eqType) (a b : X) (xs : seq X),
index a xs = index b xs ->
a \in xs -> b \in xs -> a = b
  Proof.
forall (X : eqType) (a b : X) (xs : seq X),
index a xs = index b xs ->
a \in xs -> b \in xs -> a = b
    move=> X a b xs EQ IN_a IN_b.
X: eqType
a, b: X
xs: seq X
EQ: index a xs = index b xs
IN_a: a \in xs
IN_b: b \in xs
a = b
    move: (nth_index a IN_a) => EQ_a.
X: eqType
a, b: X
xs: seq X
EQ: index a xs = index b xs
IN_a: a \in xs
IN_b: b \in xs
EQ_a: nth a xs (index a xs) = a
a = b
    move: (nth_index a IN_b) => EQ_b.
X: eqType
a, b: X
xs: seq X
EQ: index a xs = index b xs
IN_a: a \in xs
IN_b: b \in xs
EQ_a: nth a xs (index a xs) = a
EQ_b: nth a xs (index b xs) = b
a = b
    by rewrite -EQ_a -EQ_b EQ.
  Qed.

  (** We show that the nth element in a sequence is either in the
      sequence or is the default element. *)
  Lemma default_or_in :
    forall {X : eqType} (n : nat) (d : X) (xs : seq X),
      nth d xs n = d \/ nth d xs n \in xs.
forall (X : eqType) (n : nat) (d : X) (xs : seq X),
nth d xs n = d \/ nth d xs n \in xs
  Proof.
forall (X : eqType) (n : nat) (d : X) (xs : seq X),
nth d xs n = d \/ nth d xs n \in xs
    move=> x n d xs; destruct (leqP (size xs) n).
x: eqType
n: nat
d: x
xs: seq x
i: size xs <= n
nth d xs n = d \/ nth d xs n \in xs
x: eqType
n: nat
d: x
xs: seq x
i: n < size xs
nth d xs n = d \/ nth d xs n \in xs
    -
x: eqType
n: nat
d: x
xs: seq x
i: size xs <= n
nth d xs n = d \/ nth d xs n \in xs by left; apply nth_default.
    -
x: eqType
n: nat
d: x
xs: seq x
i: n < size xs
nth d xs n = d \/ nth d xs n \in xs by right; apply mem_nth.
  Qed.

  (** We show that in a unique sequence of size greater than one
      there exist two unique elements.  *)
  Lemma exists_two :
    forall {X : eqType} (xs : seq X),
      size xs > 1 ->
      uniq xs ->
      exists a b, a <> b /\ a \in xs /\ b \in xs.
forall (X : eqType) (xs : seq X),
1 < size xs ->
uniq xs ->
exists a b : X, a <> b /\ a \in xs /\ b \in xs
  Proof.
forall (X : eqType) (xs : seq X),
1 < size xs ->
uniq xs ->
exists a b : X, a <> b /\ a \in xs /\ b \in xs
    move=> T xs GT1 UNIQ.
T: eqType
xs: seq T
GT1: 1 < size xs
UNIQ: uniq xs
exists a b : T, a <> b /\ a \in xs /\ b \in xs
    (* get an element of [T] so that we can use nth *)
    have HEAD: exists x, ohead xs = Some x by elim: xs GT1 UNIQ => // a l _ _ _; exists a => //.
T: eqType
xs: seq T
GT1: 1 < size xs
UNIQ: uniq xs
HEAD: exists x : T, ohead xs = Some x
exists a b : T, a <> b /\ a \in xs /\ b \in xs
    move: (HEAD) => [x0 _].
T: eqType
xs: seq T
GT1: 1 < size xs
UNIQ: uniq xs
HEAD: exists x : T, ohead xs = Some x
x0: T
exists a b : T, a <> b /\ a \in xs /\ b \in xs
    have GT0 : 0 < size xs by exact: ltn_trans GT1.
T: eqType
xs: seq T
GT1: 1 < size xs
UNIQ: uniq xs
HEAD: exists x : T, ohead xs = Some x
x0: T
GT0: 0 < size xs
exists a b : T, a <> b /\ a \in xs /\ b \in xs
    exists (nth x0 xs 0).
T: eqType
xs: seq T
GT1: 1 < size xs
UNIQ: uniq xs
HEAD: exists x : T, ohead xs = Some x
x0: T
GT0: 0 < size xs
exists b : T,
  nth x0 xs 0 <> b /\ nth x0 xs 0 \in xs /\ b \in xs
    exists (nth x0 xs 1).
T: eqType
xs: seq T
GT1: 1 < size xs
UNIQ: uniq xs
HEAD: exists x : T, ohead xs = Some x
x0: T
GT0: 0 < size xs
nth x0 xs 0 <> nth x0 xs 1 /\
nth x0 xs 0 \in xs /\ nth x0 xs 1 \in xs
    repeat split; try apply mem_nth => //.
T: eqType
xs: seq T
GT1: 1 < size xs
UNIQ: uniq xs
HEAD: exists x : T, ohead xs = Some x
x0: T
GT0: 0 < size xs
nth x0 xs 0 <> nth x0 xs 1
    apply /eqP; apply contraNneq with (b := (0 == 1)) => // /eqP.
T: eqType
xs: seq T
GT1: 1 < size xs
UNIQ: uniq xs
HEAD: exists x : T, ohead xs = Some x
x0: T
GT0: 0 < size xs
nth x0 xs 0 == nth x0 xs 1 -> 0 == 1
    by rewrite nth_uniq.
  Qed.


  (** The predicate [all] implies the predicate [has], if the sequence is not empty. *)
  Lemma has_all_nilp {T : eqType}:
    forall (s : seq T) (P : pred T),
      all P s ->
      ~~ nilp s ->
      has P s.
T: eqType
forall (s : seq T) (P : pred T),
all P s -> ~~ nilp s -> has P s
  Proof.
T: eqType
forall (s : seq T) (P : pred T),
all P s -> ~~ nilp s -> has P s
    case => // a s P /allP ALL _.
T: eqType
a: T
s: seq T
P: pred T
ALL: {in a :: s, forall x : T, P x}
has P (a :: s)
    by apply /hasP; exists a; [|move: (ALL a); apply]; exact: mem_head.
  Qed.

End AdditionalLemmas.


(** Additional lemmas about [sorted]. *)
Section Sorted.

  (** We show that if [[x | x ∈ xs : P x]] is sorted with respect to
      values of some function [f], then it can be split into two parts:
      [[x | x ∈ xs : P x /\ f x <= t]] and [[x | x ∈ xs : P x /\ f x <= t]]. *)
  Lemma sorted_split :
    forall {X : eqType} (xs : seq X) P f t,
      sorted (fun x y => f x <= f y) xs ->
      [seq x <- xs | P x] = [seq x <- xs | P x & f x <= t] ++ [seq x <- xs | P x & f x > t].
forall (X : eqType) (xs : seq X) (P : X -> bool)
  (f : X -> nat) (t : nat),
sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
  Proof.
forall (X : eqType) (xs : seq X) (P : X -> bool)
  (f : X -> nat) (t : nat),
sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
    clear; move=> X xs P f t; elim: xs => [//|a xs IHxs] /= SORT.
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
(if P a
 then a :: [seq x <- xs | P x]
 else [seq x <- xs | P x]) =
(if P a && (f a <= t)
 then a :: [seq x <- xs | P x & f x <= t]
 else [seq x <- xs | P x & f x <= t]) ++
(if P a && (t < f a)
 then a :: [seq x <- xs | P x & t < f x]
 else [seq x <- xs | P x & t < f x])
    have TR : transitive (T:=X) (fun x y : X => f x <= f y).
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
transitive (T:=X) (fun x y : X => f x <= f y)
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
TR: transitive (T:=X) (fun x y : X => f x <= f y)
(if P a
 then a :: [seq x <- xs | P x]
 else [seq x <- xs | P x]) =
(if P a && (f a <= t)
 then a :: [seq x <- xs | P x & f x <= t]
 else [seq x <- xs | P x & f x <= t]) ++
(if P a && (t < f a)
 then a :: [seq x <- xs | P x & t < f x]
 else [seq x <- xs | P x & t < f x])
    {
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
transitive (T:=X) (fun x y : X => f x <= f y) intros ? ? ? LE1 LE2; lia. }
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
TR: transitive (T:=X) (fun x y : X => f x <= f y)
(if P a
 then a :: [seq x <- xs | P x]
 else [seq x <- xs | P x]) =
(if P a && (f a <= t)
 then a :: [seq x <- xs | P x & f x <= t]
 else [seq x <- xs | P x & f x <= t]) ++
(if P a && (t < f a)
 then a :: [seq x <- xs | P x & t < f x]
 else [seq x <- xs | P x & t < f x])
    destruct (P a) eqn:Pa, (leqP (f a) t) as [R1 | R1]; simpl.
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
TR: transitive (T:=X) (fun x y : X => f x <= f y)
Pa: P a = true
R1: f a <= t
a :: [seq x <- xs | P x] =
a
:: [seq x <- xs | P x & f x <= t] ++
   [seq x <- xs | P x & t < f x]
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
TR: transitive (T:=X) (fun x y : X => f x <= f y)
Pa: P a = true
R1: t < f a
a :: [seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
a :: [seq x <- xs | P x & t < f x]
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
TR: transitive (T:=X) (fun x y : X => f x <= f y)
Pa: P a = false
R1: f a <= t
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
TR: transitive (T:=X) (fun x y : X => f x <= f y)
Pa: P a = false
R1: t < f a
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
    {
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
TR: transitive (T:=X) (fun x y : X => f x <= f y)
Pa: P a = true
R1: f a <= t
a :: [seq x <- xs | P x] =
a
:: [seq x <- xs | P x & f x <= t] ++
   [seq x <- xs | P x & t < f x] erewrite IHxs; first by reflexivity.
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
TR: transitive (T:=X) (fun x y : X => f x <= f y)
Pa: P a = true
R1: f a <= t
sorted (fun x y : X => f x <= f y) xs
      by eapply path_sorted; eauto. }
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
TR: transitive (T:=X) (fun x y : X => f x <= f y)
Pa: P a = true
R1: t < f a
a :: [seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
a :: [seq x <- xs | P x & t < f x]
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
TR: transitive (T:=X) (fun x y : X => f x <= f y)
Pa: P a = false
R1: f a <= t
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
TR: transitive (T:=X) (fun x y : X => f x <= f y)
Pa: P a = false
R1: t < f a
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
    {
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
TR: transitive (T:=X) (fun x y : X => f x <= f y)
Pa: P a = true
R1: t < f a
a :: [seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
a :: [seq x <- xs | P x & t < f x] erewrite IHxs; last by eapply path_sorted; eauto.
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
TR: transitive (T:=X) (fun x y : X => f x <= f y)
Pa: P a = true
R1: t < f a
a
:: [seq x <- xs | P x & f x <= t] ++
   [seq x <- xs | P x & t < f x] =
[seq x <- xs | P x & f x <= t] ++
a :: [seq x <- xs | P x & t < f x]
      replace ([seq x <- xs | P x & f x <= t]) with (@nil X); first by done.
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
TR: transitive (T:=X) (fun x y : X => f x <= f y)
Pa: P a = true
R1: t < f a
[::] = [seq x <- xs | P x & f x <= t]
      symmetry; move: SORT; rewrite path_sortedE // => /andP [ALL SORT].
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
TR: transitive (T:=X) (fun x y : X => f x <= f y)
Pa: P a = true
R1: t < f a
ALL: all (fun y : X => f a <= f y) xs
SORT: sorted (fun x y : X => f x <= f y) xs
[seq x <- xs | P x & f x <= t] = [::]
      apply filter_in_pred0; intros ? IN; apply/negP; intros H; move: H => /andP [Px LEx].
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
TR: transitive (T:=X) (fun x y : X => f x <= f y)
Pa: P a = true
R1: t < f a
ALL: all (fun y : X => f a <= f y) xs
SORT: sorted (fun x y : X => f x <= f y) xs
x: X
IN: x \in xs
Px: P x
LEx: f x <= t
False
      by move: ALL => /allP ALL; specialize (ALL _ IN); simpl in ALL; lia.
    }
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
TR: transitive (T:=X) (fun x y : X => f x <= f y)
Pa: P a = false
R1: f a <= t
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
TR: transitive (T:=X) (fun x y : X => f x <= f y)
Pa: P a = false
R1: t < f a
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
    {
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
TR: transitive (T:=X) (fun x y : X => f x <= f y)
Pa: P a = false
R1: f a <= t
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] by eapply IHxs, path_sorted; eauto. }
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
TR: transitive (T:=X) (fun x y : X => f x <= f y)
Pa: P a = false
R1: t < f a
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
    {
X: eqType
P: X -> bool
f: X -> nat
t: nat
a: X
xs: seq X
IHxs: sorted (fun x y : X => f x <= f y) xs ->
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x]
SORT: path (fun x y : X => f x <= f y) a xs
TR: transitive (T:=X) (fun x y : X => f x <= f y)
Pa: P a = false
R1: t < f a
[seq x <- xs | P x] =
[seq x <- xs | P x & f x <= t] ++
[seq x <- xs | P x & t < f x] by eapply IHxs, path_sorted; eauto. }
  Qed.

  (** We show that if a sequence [xs1 ++ xs2] is sorted, then both
      subsequences [xs1] and [xs2] are sorted as well. *)
  Lemma sorted_cat:
    forall {X : eqType} {R : rel X} (xs1 xs2 : seq X),
      transitive R ->
      sorted R (xs1 ++ xs2) -> sorted R xs1 /\ sorted R xs2.
forall (X : eqType) (R : rel X) (xs1 xs2 : seq X),
transitive (T:=X) R ->
sorted R (xs1 ++ xs2) -> sorted R xs1 /\ sorted R xs2
  Proof.
forall (X : eqType) (R : rel X) (xs1 xs2 : seq X),
transitive (T:=X) R ->
sorted R (xs1 ++ xs2) -> sorted R xs1 /\ sorted R xs2
    move=> X R; elim=> [//|a xs1 IHxs1] xs2 TR SORT; split.
X: eqType
R: rel X
a: X
xs1: seq X
IHxs1: forall xs2 : seq X,
transitive (T:=X) R ->
sorted R (xs1 ++ xs2) ->
sorted R xs1 /\ sorted R xs2
xs2: seq X
TR: transitive (T:=X) R
SORT: sorted R ((a :: xs1) ++ xs2)
sorted R (a :: xs1)
X: eqType
R: rel X
a: X
xs1: seq X
IHxs1: forall xs2 : seq X,
transitive (T:=X) R ->
sorted R (xs1 ++ xs2) ->
sorted R xs1 /\ sorted R xs2
xs2: seq X
TR: transitive (T:=X) R
SORT: sorted R ((a :: xs1) ++ xs2)
sorted R xs2
    {
X: eqType
R: rel X
a: X
xs1: seq X
IHxs1: forall xs2 : seq X,
transitive (T:=X) R ->
sorted R (xs1 ++ xs2) ->
sorted R xs1 /\ sorted R xs2
xs2: seq X
TR: transitive (T:=X) R
SORT: sorted R ((a :: xs1) ++ xs2)
sorted R (a :: xs1) move: SORT; rewrite /= path_sortedE// all_cat => /andP[/andP[ALL1 ALL2] SORT].
X: eqType
R: rel X
a: X
xs1: seq X
IHxs1: forall xs2 : seq X,
transitive (T:=X) R ->
sorted R (xs1 ++ xs2) ->
sorted R xs1 /\ sorted R xs2
xs2: seq X
TR: transitive (T:=X) R
ALL1: all (R a) xs1
ALL2: all (R a) xs2
SORT: sorted R (xs1 ++ xs2)
path R a xs1
      rewrite path_sortedE//; apply/andP; split=> //.
X: eqType
R: rel X
a: X
xs1: seq X
IHxs1: forall xs2 : seq X,
transitive (T:=X) R ->
sorted R (xs1 ++ xs2) ->
sorted R xs1 /\ sorted R xs2
xs2: seq X
TR: transitive (T:=X) R
ALL1: all (R a) xs1
ALL2: all (R a) xs2
SORT: sorted R (xs1 ++ xs2)
sorted R xs1
      exact: (proj1 (IHxs1 _ _ SORT)).
    }
X: eqType
R: rel X
a: X
xs1: seq X
IHxs1: forall xs2 : seq X,
transitive (T:=X) R ->
sorted R (xs1 ++ xs2) ->
sorted R xs1 /\ sorted R xs2
xs2: seq X
TR: transitive (T:=X) R
SORT: sorted R ((a :: xs1) ++ xs2)
sorted R xs2
    {
X: eqType
R: rel X
a: X
xs1: seq X
IHxs1: forall xs2 : seq X,
transitive (T:=X) R ->
sorted R (xs1 ++ xs2) ->
sorted R xs1 /\ sorted R xs2
xs2: seq X
TR: transitive (T:=X) R
SORT: sorted R ((a :: xs1) ++ xs2)
sorted R xs2 simpl in *; move: SORT; rewrite //= path_sortedE // all_cat => /andP [/andP [ALL1 ALL2] SORT].
X: eqType
R: rel X
a: X
xs1: seq X
IHxs1: forall xs2 : seq X,
transitive (T:=X) R ->
sorted R (xs1 ++ xs2) ->
sorted R xs1 /\ sorted R xs2
xs2: seq X
TR: transitive (T:=X) R
ALL1: all (R a) xs1
ALL2: all (R a) xs2
SORT: sorted R (xs1 ++ xs2)
sorted R xs2
      by apply IHxs1.
    }
  Qed.

End Sorted.

(** Additional lemmas about [last]. *)
Section Last.

  (** First, we show that the default element does not change the
      value of [last] for non-empty sequences.  *)
  Lemma nonnil_last :
    forall {X : eqType} (xs : seq X) (d1 d2 : X),
      xs != [::] ->
      last d1 xs = last d2 xs.
forall (X : eqType) (xs : seq X) (d1 d2 : X),
xs != [::] -> last d1 xs = last d2 xs
  Proof.
forall (X : eqType) (xs : seq X) (d1 d2 : X),
xs != [::] -> last d1 xs = last d2 xs by move=> X xs d1 d2; elim: xs => [//|a xs IHxs] _. Qed.

  (** We show that if a sequence [xs] contains an element that
      satisfies a predicate [P], then the last element of [filter P xs]
      is in [xs]. *)
  Lemma filter_last_mem :
    forall {X : eqType} (xs : seq X) (d : X) (P : pred X),
      has P xs ->
      last d (filter P xs) \in xs.
forall (X : eqType) (xs : seq X) (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
  Proof.
forall (X : eqType) (xs : seq X) (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
    move=> X; elim=> [//|a xs IHxs] d P /hasP [x + Px].
X: eqType
a: X
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
x \in a :: xs ->
last d [seq x <- a :: xs | P x] \in a :: xs
    rewrite in_cons => /orP [/eqP EQ | IN].
X: eqType
a: X
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
EQ: x = a
last d [seq x <- a :: xs | P x] \in a :: xs
X: eqType
a: X
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
IN: x \in xs
last d [seq x <- a :: xs | P x] \in a :: xs
    {
X: eqType
a: X
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
EQ: x = a
last d [seq x <- a :: xs | P x] \in a :: xs simpl; subst a; rewrite Px; simpl.
X: eqType
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
last x [seq x <- xs | P x] \in x :: xs
      destruct (has P xs) eqn:HAS.
X: eqType
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
HAS: has P xs = true
last x [seq x <- xs | P x] \in x :: xs
X: eqType
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
HAS: has P xs = false
last x [seq x <- xs | P x] \in x :: xs
      {
X: eqType
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
HAS: has P xs = true
last x [seq x <- xs | P x] \in x :: xs by rewrite in_cons; apply/orP; right; apply IHxs. }
X: eqType
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
HAS: has P xs = false
last x [seq x <- xs | P x] \in x :: xs
      {
X: eqType
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
HAS: has P xs = false
last x [seq x <- xs | P x] \in x :: xs replace (filter _ _) with (@nil X).
X: eqType
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
HAS: has P xs = false
last x [::] \in x :: xs
X: eqType
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
HAS: has P xs = false
[::] = [seq x <- xs | P x]
        -
X: eqType
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
HAS: has P xs = false
last x [::] \in x :: xs by simpl; rewrite in_cons; apply/orP; left.
        -
X: eqType
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
HAS: has P xs = false
[::] = [seq x <- xs | P x] symmetry; apply filter_in_pred0; intros y IN.
X: eqType
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
HAS: has P xs = false
y: X
IN: y \in xs
~~ P y
          by move: HAS => /negP/negP/hasPn ALLN; apply: ALLN.
      }
    }
X: eqType
a: X
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
IN: x \in xs
last d [seq x <- a :: xs | P x] \in a :: xs
    {
X: eqType
a: X
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
IN: x \in xs
last d [seq x <- a :: xs | P x] \in a :: xs rewrite in_cons; apply/orP; right.
X: eqType
a: X
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
IN: x \in xs
last d [seq x <- a :: xs | P x] \in xs
      simpl; destruct (P a); simpl; apply IHxs.
X: eqType
a: X
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
IN: x \in xs
has P xs
X: eqType
a: X
xs: seq X
IHxs: forall (d : X) (P : pred X),
has P xs -> last d [seq x <- xs | P x] \in xs
d: X
P: pred X
x: X
Px: P x
IN: x \in xs
has P xs
      all: by apply/hasP; exists x.
    }
  Qed.

End Last.



(** Function [rem] from [ssreflect] removes only the first occurrence of
    an element in a sequence.  We define function [rem_all] which
    removes all occurrences of an element in a sequence. *)
Fixpoint rem_all {X : eqType} (x : X) (xs : seq X) :=
  match xs with
  | [::] => [::]
  | a :: xs =>
    if a == x then rem_all x xs else a :: rem_all x xs
  end.

(** Additional lemmas about [rem_all] for lists. *)
Section RemAllList.

  (** First we prove that [x ∉ rem_all x xs]. *)
  Lemma nin_rem_all :
    forall {X : eqType} (x : X) (xs : seq X),
      ~ (x \in rem_all x xs).
forall (X : eqType) (x : X) (xs : seq X),
~ x \in rem_all x xs
  Proof.
forall (X : eqType) (x : X) (xs : seq X),
~ x \in rem_all x xs
    move=> X x; elim=> [//|a xs IHxs] IN.
X: eqType
x, a: X
xs: seq X
IHxs: ~ x \in rem_all x xs
IN: x \in rem_all x (a :: xs)
False
    apply: IHxs.
X: eqType
x, a: X
xs: seq X
IN: x \in rem_all x (a :: xs)
x \in rem_all x xs
    simpl in IN; destruct (a == x) eqn:EQ; first by done.
X: eqType
x, a: X
xs: seq X
EQ: (a == x) = false
IN: x \in a :: rem_all x xs
x \in rem_all x xs
    move: IN; rewrite in_cons; move => /orP [/eqP EQ2 | IN]; last by done.
X: eqType
x, a: X
xs: seq X
EQ: (a == x) = false
EQ2: x = a
x \in rem_all x xs
    by subst; exfalso; rewrite eq_refl in EQ.
  Qed.

  (** Next we show that [rem_all x xs ⊆ xs].  *)
  Lemma in_rem_all :
    forall {X : eqType} (a x : X) (xs : seq X),
      a \in rem_all x xs -> a \in xs.
forall (X : eqType) (a x : X) (xs : seq X),
a \in rem_all x xs -> a \in xs
  Proof.
forall (X : eqType) (a x : X) (xs : seq X),
a \in rem_all x xs -> a \in xs
    intros X a x; elim=> [//|a0 xs IHxs] /= IN.
X: eqType
a, x, a0: X
xs: seq X
IHxs: a \in rem_all x xs -> a \in xs
IN: a
  \in (if a0 == x
       then rem_all x xs
       else a0 :: rem_all x xs)
a \in a0 :: xs
    destruct (a0 == x) eqn:EQ.
X: eqType
a, x, a0: X
xs: seq X
IHxs: a \in rem_all x xs -> a \in xs
EQ: (a0 == x) = true
IN: a \in rem_all x xs
a \in a0 :: xs
X: eqType
a, x, a0: X
xs: seq X
IHxs: a \in rem_all x xs -> a \in xs
EQ: (a0 == x) = false
IN: a \in a0 :: rem_all x xs
a \in a0 :: xs
    -
X: eqType
a, x, a0: X
xs: seq X
IHxs: a \in rem_all x xs -> a \in xs
EQ: (a0 == x) = true
IN: a \in rem_all x xs
a \in a0 :: xs by rewrite in_cons; apply/orP; right; eauto.
    -
X: eqType
a, x, a0: X
xs: seq X
IHxs: a \in rem_all x xs -> a \in xs
EQ: (a0 == x) = false
IN: a \in a0 :: rem_all x xs
a \in a0 :: xs move: IN; rewrite in_cons; move => /orP [EQ2|IN].
X: eqType
a, x, a0: X
xs: seq X
IHxs: a \in rem_all x xs -> a \in xs
EQ: (a0 == x) = false
EQ2: a == a0
a \in a0 :: xs
X: eqType
a, x, a0: X
xs: seq X
IHxs: a \in rem_all x xs -> a \in xs
EQ: (a0 == x) = false
IN: a \in rem_all x xs
a \in a0 :: xs
      +
X: eqType
a, x, a0: X
xs: seq X
IHxs: a \in rem_all x xs -> a \in xs
EQ: (a0 == x) = false
EQ2: a == a0
a \in a0 :: xs by rewrite in_cons; apply/orP; left.
      +
X: eqType
a, x, a0: X
xs: seq X
IHxs: a \in rem_all x xs -> a \in xs
EQ: (a0 == x) = false
IN: a \in rem_all x xs
a \in a0 :: xs by rewrite in_cons; apply/orP; right; auto.
  Qed.

  (** If an element [x] is smaller than any element of
      a sequence [xs], then [rem_all x xs = xs]. *)
  Lemma rem_lt_id :
    forall x xs,
      (forall y, y \in xs -> x < y) ->
      rem_all x xs = xs.
forall (x : nat)
  (xs : seq_predType
          Datatypes_nat__canonical__eqtype_Equality),
(forall y : nat, y \in xs -> x < y) ->
rem_all x xs = xs
  Proof.
forall (x : nat)
  (xs : seq_predType
          Datatypes_nat__canonical__eqtype_Equality),
(forall y : nat, y \in xs -> x < y) ->
rem_all x xs = xs
    move=> x; elim=> [//|a xs IHxs] MIN /=.
x: nat
a: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: (forall y : nat, y \in xs -> x < y) ->
rem_all x xs = xs
MIN: forall y : nat, y \in a :: xs -> x < y
(if a == x then rem_all x xs else a :: rem_all x xs) =
a :: xs
    have -> : (a == x) = false.
x: nat
a: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: (forall y : nat, y \in xs -> x < y) ->
rem_all x xs = xs
MIN: forall y : nat, y \in a :: xs -> x < y
(a == x) = false
x: nat
a: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: (forall y : nat, y \in xs -> x < y) ->
rem_all x xs = xs
MIN: forall y : nat, y \in a :: xs -> x < y
a :: rem_all x xs = a :: xs
    {
x: nat
a: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: (forall y : nat, y \in xs -> x < y) ->
rem_all x xs = xs
MIN: forall y : nat, y \in a :: xs -> x < y
(a == x) = false apply/eqP/eqP; rewrite neq_ltn; apply/orP; right.
x: nat
a: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: (forall y : nat, y \in xs -> x < y) ->
rem_all x xs = xs
MIN: forall y : nat, y \in a :: xs -> x < y
x < a
      by apply MIN; rewrite in_cons; apply/orP; left.
    }
x: nat
a: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: (forall y : nat, y \in xs -> x < y) ->
rem_all x xs = xs
MIN: forall y : nat, y \in a :: xs -> x < y
a :: rem_all x xs = a :: xs
    rewrite IHxs //.
x: nat
a: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: (forall y : nat, y \in xs -> x < y) ->
rem_all x xs = xs
MIN: forall y : nat, y \in a :: xs -> x < y
forall y : nat, y \in xs -> x < y
    intros; apply: MIN.
x: nat
a: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: (forall y : nat, y \in xs -> x < y) ->
rem_all x xs = xs
y: nat
H: y \in xs
y \in a :: xs
    by rewrite in_cons; apply/orP; right.
  Qed.

End RemAllList.

(** To have a more intuitive naming, we introduce the definition of
    [range a b] which is equal to [index_iota a b.+1]. *)
Definition range (a b : nat) := index_iota a b.+1.

(** Additional lemmas about [index_iota] and [range] for lists. *)
Section IotaRange.

  (** First, we show that [iota m n] can be split into two parts
      [iota m nle] and [iota (m + nle) (n - nle)] for any [nle <= n]. *)
  Lemma iotaD_impl :
    forall n_le m n,
      n_le <= n ->
      iota m n = iota m n_le ++ iota (m + n_le) (n - n_le).
forall n_le m n : nat,
n_le <= n ->
iota m n = iota m n_le ++ iota (m + n_le) (n - n_le)
  Proof.
forall n_le m n : nat,
n_le <= n ->
iota m n = iota m n_le ++ iota (m + n_le) (n - n_le)
    move=> n_le m n LE.
n_le, m, n: nat
LE: n_le <= n
iota m n = iota m n_le ++ iota (m + n_le) (n - n_le)
    interval_to_duration n_le n k.
n_le, m, k: nat
iota m (n_le + k) =
iota m n_le ++ iota (m + n_le) (n_le + k - n_le)
    by rewrite iotaD; replace (_ + _ - _) with k; last lia.
  Qed.

  (** Next, we prove that [index_iota a b = a :: index_iota a.+1 b]
      for [a < b]. *)
  Remark index_iota_lt_step :
    forall a b,
      a < b ->
      index_iota a b = a :: index_iota a.+1 b.
forall a b : nat,
a < b -> index_iota a b = a :: index_iota a.+1 b
  Proof.
forall a b : nat,
a < b -> index_iota a b = a :: index_iota a.+1 b
    move=> a b LT; unfold index_iota.
a, b: nat
LT: a < b
iota a (b - a) = a :: iota a.+1 (b - a.+1)
    destruct b; first by done.
a, b: nat
LT: a < b.+1
iota a (b.+1 - a) = a :: iota a.+1 (b.+1 - a.+1)
    rewrite ltnS in LT.
a, b: nat
LT: a <= b
iota a (b.+1 - a) = a :: iota a.+1 (b.+1 - a.+1)
    by rewrite subSn //.
  Qed.

  (** We prove that one can remove duplicating element from the
      head of a sequence by which [range] is filtered. *)
  Lemma range_filter_2cons :
    forall x xs k,
      [seq ρ <- range 0 k | ρ \in x :: x :: xs] =
      [seq ρ <- range 0 k | ρ \in x :: xs].
forall (x : Datatypes_nat__canonical__eqtype_Equality)
  (xs : seq Datatypes_nat__canonical__eqtype_Equality)
  (k : nat),
[seq ρ <- range 0 k | ρ \in [:: x, x & xs]] =
[seq ρ <- range 0 k | ρ \in x :: xs]
  Proof.
forall (x : Datatypes_nat__canonical__eqtype_Equality)
  (xs : seq Datatypes_nat__canonical__eqtype_Equality)
  (k : nat),
[seq ρ <- range 0 k | ρ \in [:: x, x & xs]] =
[seq ρ <- range 0 k | ρ \in x :: xs]
    move=> x xs k; apply: eq_filter => x0.
x: Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
k: nat
x0: Datatypes_nat__canonical__eqtype_Equality
(x0 \in [:: x, x & xs]) = (x0 \in x :: xs)
    by rewrite !in_cons; destruct (x0 == x), (x0 \in xs).
  Qed.

  (** Consider [a], [b], and [x] s.t. [a ≤ x < b],
      then filter of [iota_index a b] with predicate
      [(_ == x)] yields [::x]. *)
  Lemma index_iota_filter_eqx :
    forall x a b,
      a <= x < b ->
      [seq ρ <- index_iota a b | ρ == x] = [::x].
forall x a b : nat,
a <= x < b ->
[seq ρ <- index_iota a b | ρ == x] = [:: x]
  Proof.
forall x a b : nat,
a <= x < b ->
[seq ρ <- index_iota a b | ρ == x] = [:: x]
    move=> x a b.
x, a, b: nat
a <= x < b ->
[seq ρ <- index_iota a b | ρ == x] = [:: x]
    have EX : exists k, b - a <= k.
x, a, b: nat
exists k : nat, b - a <= k
x, a, b: nat
EX: exists k : nat, b - a <= k
a <= x < b ->
[seq ρ <- index_iota a b | ρ == x] = [:: x]
    {
x, a, b: nat
exists k : nat, b - a <= k exists (b-a); by simpl. }
x, a, b: nat
EX: exists k : nat, b - a <= k
a <= x < b ->
[seq ρ <- index_iota a b | ρ == x] = [:: x]
    destruct EX as [k BO].
x, a, b, k: nat
BO: b - a <= k
a <= x < b ->
[seq ρ <- index_iota a b | ρ == x] = [:: x]
    revert x a b BO; elim: k => [|k IHk] => x a b BO /andP [GE LT].
x, a, b: nat
BO: b - a <= 0
GE: a <= x
LT: x < b
[seq ρ <- index_iota a b | ρ == x] = [:: x]
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
x, a, b: nat
BO: b - a <= k.+1
GE: a <= x
LT: x < b
[seq ρ <- index_iota a b | ρ == x] = [:: x]
    {
x, a, b: nat
BO: b - a <= 0
GE: a <= x
LT: x < b
[seq ρ <- index_iota a b | ρ == x] = [:: x] by exfalso; move: BO; rewrite leqn0 subn_eq0; move => BO; lia. }
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
x, a, b: nat
BO: b - a <= k.+1
GE: a <= x
LT: x < b
[seq ρ <- index_iota a b | ρ == x] = [:: x]
    {
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
x, a, b: nat
BO: b - a <= k.+1
GE: a <= x
LT: x < b
[seq ρ <- index_iota a b | ρ == x] = [:: x] destruct a as [|a].
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
x, b: nat
BO: b - 0 <= k.+1
GE: 0 <= x
LT: x < b
[seq ρ <- index_iota 0 b | ρ == x] = [:: x]
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
x, a, b: nat
BO: b - a.+1 <= k.+1
GE: a < x
LT: x < b
[seq ρ <- index_iota a.+1 b | ρ == x] = [:: x]
      {
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
x, b: nat
BO: b - 0 <= k.+1
GE: 0 <= x
LT: x < b
[seq ρ <- index_iota 0 b | ρ == x] = [:: x] destruct b; first by done.
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
x, b: nat
BO: b.+1 - 0 <= k.+1
GE: 0 <= x
LT: x < b.+1
[seq ρ <- index_iota 0 b.+1 | ρ == x] = [:: x]
        rewrite index_iota_lt_step //; simpl.
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
x, b: nat
BO: b.+1 - 0 <= k.+1
GE: 0 <= x
LT: x < b.+1
(if 0 == x
 then 0 :: [seq ρ <- index_iota 1 b.+1 | ρ == x]
 else [seq ρ <- index_iota 1 b.+1 | ρ == x]) = [:: x]
        destruct (0 == x) eqn:EQ.
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
x, b: nat
BO: b.+1 - 0 <= k.+1
GE: 0 <= x
LT: x < b.+1
EQ: (0 == x) = true
0 :: [seq ρ <- index_iota 1 b.+1 | ρ == x] = [:: x]
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
x, b: nat
BO: b.+1 - 0 <= k.+1
GE: 0 <= x
LT: x < b.+1
EQ: (0 == x) = false
[seq ρ <- index_iota 1 b.+1 | ρ == x] = [:: x]
        -
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
x, b: nat
BO: b.+1 - 0 <= k.+1
GE: 0 <= x
LT: x < b.+1
EQ: (0 == x) = true
0 :: [seq ρ <- index_iota 1 b.+1 | ρ == x] = [:: x] move: EQ => /eqP EQ; subst x.
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
b: nat
BO: b.+1 - 0 <= k.+1
LT: 0 < b.+1
GE: 0 <= 0
0 :: [seq ρ <- index_iota 1 b.+1 | ρ == 0] = [:: 0]
          rewrite filter_in_pred0 //.
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
b: nat
BO: b.+1 - 0 <= k.+1
LT: 0 < b.+1
GE: 0 <= 0
forall x : Datatypes_nat__canonical__eqtype_Equality,
x \in index_iota 1 b.+1 -> x != 0
          by intros x; rewrite mem_index_iota -lt0n; move => /andP [T1 _].
        -
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
x, b: nat
BO: b.+1 - 0 <= k.+1
GE: 0 <= x
LT: x < b.+1
EQ: (0 == x) = false
[seq ρ <- index_iota 1 b.+1 | ρ == x] = [:: x] by apply IHk; lia.
      }
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
x, a, b: nat
BO: b - a.+1 <= k.+1
GE: a < x
LT: x < b
[seq ρ <- index_iota a.+1 b | ρ == x] = [:: x]
      rewrite index_iota_lt_step; last by lia.
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
x, a, b: nat
BO: b - a.+1 <= k.+1
GE: a < x
LT: x < b
[seq ρ <- a.+1 :: index_iota a.+2 b | ρ == x] = [:: x]
      simpl; destruct (a.+1 == x) eqn:EQ.
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
x, a, b: nat
BO: b - a.+1 <= k.+1
GE: a < x
LT: x < b
EQ: (a.+1 == x) = true
a.+1 :: [seq ρ <- index_iota a.+2 b | ρ == x] = [:: x]
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
x, a, b: nat
BO: b - a.+1 <= k.+1
GE: a < x
LT: x < b
EQ: (a.+1 == x) = false
[seq ρ <- index_iota a.+2 b | ρ == x] = [:: x]
      -
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
x, a, b: nat
BO: b - a.+1 <= k.+1
GE: a < x
LT: x < b
EQ: (a.+1 == x) = true
a.+1 :: [seq ρ <- index_iota a.+2 b | ρ == x] = [:: x] move: EQ => /eqP EQ; subst x.
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
a, b: nat
BO: b - a.+1 <= k.+1
LT: a.+1 < b
GE: a < a.+1
a.+1 :: [seq ρ <- index_iota a.+2 b | ρ == a.+1] =
[:: a.+1]
        rewrite filter_in_pred0 //.
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
a, b: nat
BO: b - a.+1 <= k.+1
LT: a.+1 < b
GE: a < a.+1
forall x : Datatypes_nat__canonical__eqtype_Equality,
x \in index_iota a.+2 b -> x != a.+1
        intros x; rewrite mem_index_iota; move => /andP [T1 _].
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
a, b: nat
BO: b - a.+1 <= k.+1
LT: a.+1 < b
GE: a < a.+1
x: Datatypes_nat__canonical__eqtype_Equality
T1: a.+1 < x
x != a.+1
        by rewrite neq_ltn; apply/orP; right.
      -
k: nat
IHk: forall x a b : nat,
b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
x, a, b: nat
BO: b - a.+1 <= k.+1
GE: a < x
LT: x < b
EQ: (a.+1 == x) = false
[seq ρ <- index_iota a.+2 b | ρ == x] = [:: x] by rewrite IHk //; lia.
    }
  Qed.

  (** As a corollary we prove that filter of [iota_index a b]
      with predicate [(_ ∈ [::x])] yields [::x]. *)
  Corollary index_iota_filter_singl :
    forall x a b,
      a <= x < b ->
      [seq ρ <- index_iota a b | ρ \in [:: x]] = [::x].
forall x a b : nat,
a <= x < b ->
[seq ρ <- index_iota a b | ρ \in [:: x]] = [:: x]
  Proof.
forall x a b : nat,
a <= x < b ->
[seq ρ <- index_iota a b | ρ \in [:: x]] = [:: x]
    move=> x a b NEQ.
x, a, b: nat
NEQ: a <= x < b
[seq ρ <- index_iota a b | ρ \in [:: x]] = [:: x]
    rewrite -{2}(index_iota_filter_eqx _ a b) //.
x, a, b: nat
NEQ: a <= x < b
[seq ρ <- index_iota a b | ρ \in [:: x]] =
[seq ρ <- index_iota a b | ρ == x]
    apply eq_filter; intros ?.
x, a, b: nat
NEQ: a <= x < b
x0: Datatypes_nat__canonical__eqtype_Equality
(x0 \in [:: x]) = (x0 == x)
    by repeat rewrite in_cons; rewrite in_nil Bool.orb_false_r.
  Qed.

  (** Next we prove that if an element [x] is not in a sequence [xs],
      then [iota_index a b] filtered with predicate [(_ ∈ xs)] is
      equal to [iota_index a b] filtered with predicate [(_ ∈ rem_all
      x xs)]. *)
  Lemma index_iota_filter_inxs :
    forall a b x xs,
      x < a ->
      [seq ρ <- index_iota a b | ρ \in xs] =
      [seq ρ <- index_iota a b | ρ \in rem_all x xs].
forall (a b x : nat)
  (xs : seq_predType
          Datatypes_nat__canonical__eqtype_Equality),
x < a ->
[seq ρ <- index_iota a b | ρ \in xs] =
[seq ρ <- index_iota a b | ρ \in rem_all x xs]
  Proof.
forall (a b x : nat)
  (xs : seq_predType
          Datatypes_nat__canonical__eqtype_Equality),
x < a ->
[seq ρ <- index_iota a b | ρ \in xs] =
[seq ρ <- index_iota a b | ρ \in rem_all x xs]
    intros a b x xs LT.
a, b, x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
LT: x < a
[seq ρ <- index_iota a b | ρ \in xs] =
[seq ρ <- index_iota a b | ρ \in rem_all x xs]
    apply eq_in_filter.
a, b, x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
LT: x < a
{in index_iota a b,
  ssrfun.eqfun [in xs] [in rem_all x xs]}
    intros y; rewrite mem_index_iota; move => /andP [LE GT].
a, b, x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
LT: x < a
y: Datatypes_nat__canonical__eqtype_Equality
LE: a <= y
GT: y < b
(y \in xs) = (y \in rem_all x xs)
    elim: xs => [//|y' xs IHxs].
a, b, x: nat
LT: x < a
y: Datatypes_nat__canonical__eqtype_Equality
LE: a <= y
GT: y < b
y': Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
IHxs: (y \in xs) = (y \in rem_all x xs)
(y \in y' :: xs) = (y \in rem_all x (y' :: xs))
    rewrite in_cons IHxs; simpl; clear IHxs.
a, b, x: nat
LT: x < a
y: Datatypes_nat__canonical__eqtype_Equality
LE: a <= y
GT: y < b
y': Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
(y == y') || (y \in rem_all x xs) =
(y
   \in (if y' == x
        then rem_all x xs
        else y' :: rem_all x xs))
    destruct (y == y') eqn:EQ1, (y' == x) eqn:EQ2; auto.
a, b, x: nat
LT: x < a
y: Datatypes_nat__canonical__eqtype_Equality
LE: a <= y
GT: y < b
y': Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
EQ1: (y == y') = true
EQ2: (y' == x) = true
true || (y \in rem_all x xs) = (y \in rem_all x xs)
a, b, x: nat
LT: x < a
y: Datatypes_nat__canonical__eqtype_Equality
LE: a <= y
GT: y < b
y': Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
EQ1: (y == y') = true
EQ2: (y' == x) = false
true || (y \in rem_all x xs) =
(y \in y' :: rem_all x xs)
a, b, x: nat
LT: x < a
y: Datatypes_nat__canonical__eqtype_Equality
LE: a <= y
GT: y < b
y': Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
EQ1: (y == y') = false
EQ2: (y' == x) = false
false || (y \in rem_all x xs) =
(y \in y' :: rem_all x xs)
    -
a, b, x: nat
LT: x < a
y: Datatypes_nat__canonical__eqtype_Equality
LE: a <= y
GT: y < b
y': Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
EQ1: (y == y') = true
EQ2: (y' == x) = true
true || (y \in rem_all x xs) = (y \in rem_all x xs) by exfalso; move: EQ1 EQ2 => /eqP EQ1 /eqP EQ2; subst; lia.
    -
a, b, x: nat
LT: x < a
y: Datatypes_nat__canonical__eqtype_Equality
LE: a <= y
GT: y < b
y': Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
EQ1: (y == y') = true
EQ2: (y' == x) = false
true || (y \in rem_all x xs) =
(y \in y' :: rem_all x xs) by move: EQ1 => /eqP EQ1; subst; rewrite in_cons eq_refl.
    -
a, b, x: nat
LT: x < a
y: Datatypes_nat__canonical__eqtype_Equality
LE: a <= y
GT: y < b
y': Datatypes_nat__canonical__eqtype_Equality
xs: seq Datatypes_nat__canonical__eqtype_Equality
EQ1: (y == y') = false
EQ2: (y' == x) = false
false || (y \in rem_all x xs) =
(y \in y' :: rem_all x xs) by rewrite in_cons EQ1.
  Qed.

  (** We prove that if an element [x] is a min of a sequence [xs],
      then [iota_index a b] filtered with predicate [(_ ∈ x::xs)] is
      equal to [x :: iota_index a b] filtered with predicate [(_ ∈
      rem_all x xs)]. *)
  Lemma index_iota_filter_step :
    forall x xs a b,
      a <= x < b ->
      (forall y, y \in xs -> x <= y) ->
      [seq ρ <- index_iota a b | ρ \in x :: xs] =
      x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs].
forall (x : nat)
  (xs : seq_predType
          Datatypes_nat__canonical__eqtype_Equality)
  (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
  Proof.
forall (x : nat)
  (xs : seq_predType
          Datatypes_nat__canonical__eqtype_Equality)
  (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
    intros x xs a b B MIN.
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
B: a <= x < b
MIN: forall y : nat, y \in xs -> x <= y
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
    have EX : exists k, b - a <= k.
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
B: a <= x < b
MIN: forall y : nat, y \in xs -> x <= y
exists k : nat, b - a <= k
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
B: a <= x < b
MIN: forall y : nat, y \in xs -> x <= y
EX: exists k : nat, b - a <= k
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
    {
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
B: a <= x < b
MIN: forall y : nat, y \in xs -> x <= y
exists k : nat, b - a <= k exists (b-a); by simpl. }
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
B: a <= x < b
MIN: forall y : nat, y \in xs -> x <= y
EX: exists k : nat, b - a <= k
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] destruct EX as [k BO].
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
B: a <= x < b
MIN: forall y : nat, y \in xs -> x <= y
k: nat
BO: b - a <= k
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
    revert x xs a b B MIN BO.
k: nat
forall (x : nat)
  (xs : seq_predType
          Datatypes_nat__canonical__eqtype_Equality)
  (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
    elim: k => [ |k IHk] x xs a b /andP [LE GT] MIN BO.
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
LE: a <= x
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= 0
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
LE: a <= x
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
    -
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
LE: a <= x
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= 0
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] by move_neq_down BO; lia.
    -
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
LE: a <= x
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] move: LE; rewrite leq_eqVlt; move => /orP [/eqP EQ|LT].
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
EQ: a = x
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
      +
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
EQ: a = x
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] subst.
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - x <= k.+1
[seq ρ <- index_iota x b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota x b | ρ \in rem_all x xs]
        rewrite index_iota_lt_step //.
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - x <= k.+1
[seq ρ <- x :: index_iota x.+1 b | ρ \in x :: xs] =
x
:: [seq ρ <- x :: index_iota x.+1 b
      | ρ \in rem_all x xs]
        replace ([seq ρ <- x :: index_iota x.+1 b | ρ \in x :: xs])
          with (x :: [seq ρ <- index_iota x.+1 b | ρ \in x :: xs]); last first.
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - x <= k.+1
x :: [seq ρ <- index_iota x.+1 b | ρ \in x :: xs] =
[seq ρ <- x :: index_iota x.+1 b | ρ \in x :: xs]
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - x <= k.+1
x :: [seq ρ <- index_iota x.+1 b | ρ \in x :: xs] =
x
:: [seq ρ <- x :: index_iota x.+1 b
      | ρ \in rem_all x xs]
        {
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - x <= k.+1
x :: [seq ρ <- index_iota x.+1 b | ρ \in x :: xs] =
[seq ρ <- x :: index_iota x.+1 b | ρ \in x :: xs] by rewrite /= in_cons eqxx.
        }
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - x <= k.+1
x :: [seq ρ <- index_iota x.+1 b | ρ \in x :: xs] =
x
:: [seq ρ <- x :: index_iota x.+1 b
      | ρ \in rem_all x xs]
        rewrite (index_iota_filter_inxs _ _ x) //; simpl.
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - x <= k.+1
x
:: [seq ρ <- index_iota x.+1 b
      | ρ
          \in (if x == x
               then rem_all x xs
               else x :: rem_all x xs)] =
x
:: (if x \in rem_all x xs
    then
     x
     :: [seq ρ <- index_iota x.+1 b
           | ρ \in rem_all x xs]
    else
     [seq ρ <- index_iota x.+1 b | ρ \in rem_all x xs])
        rewrite eq_refl.
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - x <= k.+1
x :: [seq ρ <- index_iota x.+1 b | ρ \in rem_all x xs] =
x
:: (if x \in rem_all x xs
    then
     x
     :: [seq ρ <- index_iota x.+1 b
           | ρ \in rem_all x xs]
    else
     [seq ρ <- index_iota x.+1 b | ρ \in rem_all x xs])
        replace (@in_mem nat x (@mem nat (seq_predType _) (@rem_all _ x xs))) with false; first by reflexivity.
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - x <= k.+1
false = (x \in rem_all x xs)
        apply/eqP; rewrite eq_sym eqbF_neg.
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - x <= k.+1
x \notin rem_all x xs
        apply/negP; apply nin_rem_all.
      +
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs] rewrite index_iota_lt_step //; last by lia.
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
[seq ρ <- a :: index_iota a.+1 b | ρ \in x :: xs] =
x
:: [seq ρ <- a :: index_iota a.+1 b
      | ρ \in rem_all x xs]
        replace ([seq ρ <- a :: index_iota a.+1 b | ρ \in x :: xs])
          with ([seq ρ <- index_iota a.+1 b | ρ \in x :: xs]); last first.
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
[seq ρ <- index_iota a.+1 b | ρ \in x :: xs] =
[seq ρ <- a :: index_iota a.+1 b | ρ \in x :: xs]
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
[seq ρ <- index_iota a.+1 b | ρ \in x :: xs] =
x
:: [seq ρ <- a :: index_iota a.+1 b
      | ρ \in rem_all x xs]
        {
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
[seq ρ <- index_iota a.+1 b | ρ \in x :: xs] =
[seq ρ <- a :: index_iota a.+1 b | ρ \in x :: xs] simpl; replace (@in_mem nat a (@mem nat (seq_predType _) (@cons nat x xs))) with false; first by done.
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
false = (a \in x :: xs)
          apply/eqP; rewrite eq_sym eqbF_neg.
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
a \notin x :: xs
          apply/negP; rewrite in_cons; intros C; move: C => /orP [/eqP C|C].
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
C: a = x
False
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
C: a \in xs
False
          -
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
C: a = x
False by subst; rewrite ltnn in LT.
          -
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
C: a \in xs
False by move_neq_down LT; apply MIN.
        }
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
[seq ρ <- index_iota a.+1 b | ρ \in x :: xs] =
x
:: [seq ρ <- a :: index_iota a.+1 b
      | ρ \in rem_all x xs]
        replace ([seq ρ <- a :: index_iota a.+1 b | ρ \in rem_all x xs])
          with ([seq ρ <- index_iota a.+1 b | ρ \in rem_all x xs]); last first.
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
[seq ρ <- index_iota a.+1 b | ρ \in rem_all x xs] =
[seq ρ <- a :: index_iota a.+1 b | ρ \in rem_all x xs]
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
[seq ρ <- index_iota a.+1 b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a.+1 b | ρ \in rem_all x xs]
        {
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
[seq ρ <- index_iota a.+1 b | ρ \in rem_all x xs] =
[seq ρ <- a :: index_iota a.+1 b | ρ \in rem_all x xs] simpl; replace (@in_mem nat a (@mem nat (seq_predType _) (@rem_all _ x xs))) with false; first by done.
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
false = (a \in rem_all x xs)
          apply/eqP; rewrite eq_sym eqbF_neg; apply/negP; intros C.
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
C: a \in rem_all x xs
False
          apply in_rem_all in C.
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
C: a \in xs
False
          by move_neq_down LT; apply MIN.
        }
k: nat
IHk: forall (x : nat)
(xs : seq_predType Datatypes_nat__canonical__eqtype_Equality) (a b : nat),
a <= x < b ->
(forall y : nat, y \in xs -> x <= y) ->
b - a <= k ->
[seq ρ <- index_iota a b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
a, b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - a <= k.+1
LT: a < x
[seq ρ <- index_iota a.+1 b | ρ \in x :: xs] =
x :: [seq ρ <- index_iota a.+1 b | ρ \in rem_all x xs]
        by rewrite IHk //; lia.
  Qed.

  (** For convenience, we define a special case of
      lemma [index_iota_filter_step] for [a = 0] and [b = k.+1]. *)
  Corollary range_iota_filter_step:
    forall x xs k,
      x <= k ->
      (forall y, y \in xs -> x <= y) ->
      [seq ρ <- range 0 k | ρ \in x :: xs] =
      x :: [seq ρ <- range 0 k | ρ \in rem_all x xs].
forall (x : nat)
  (xs : seq_predType
          Datatypes_nat__canonical__eqtype_Equality)
  (k : nat),
x <= k ->
(forall y : nat, y \in xs -> x <= y) ->
[seq ρ <- range 0 k | ρ \in x :: xs] =
x :: [seq ρ <- range 0 k | ρ \in rem_all x xs]
  Proof.
forall (x : nat)
  (xs : seq_predType
          Datatypes_nat__canonical__eqtype_Equality)
  (k : nat),
x <= k ->
(forall y : nat, y \in xs -> x <= y) ->
[seq ρ <- range 0 k | ρ \in x :: xs] =
x :: [seq ρ <- range 0 k | ρ \in rem_all x xs]
    intros x xs k LE MIN.
x: nat
xs: seq_predType
  Datatypes_nat__canonical__eqtype_Equality
k: nat
LE: x <= k
MIN: forall y : nat, y \in xs -> x <= y
[seq ρ <- range 0 k | ρ \in x :: xs] =
x :: [seq ρ <- range 0 k | ρ \in rem_all x xs]
      by apply index_iota_filter_step; auto.
  Qed.

  (** We prove that if [x < a], then [x < (filter P (index_iota a
      b))[idx]] for any predicate [P]. *)
  Lemma iota_filter_gt:
    forall x a b idx P,
      x < a ->
      idx < size ([seq x <- index_iota a b | P x]) ->
      x < nth 0 [seq x <- index_iota a b | P x] idx.
forall (x a b idx : nat) (P : nat -> bool),
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
  Proof.
forall (x a b idx : nat) (P : nat -> bool),
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
    clear=> x a b idx P.
x, a, b, idx: nat
P: nat -> bool
x < a ->
idx < size [seq x <- index_iota a b | P x] ->
x < nth 0 [seq x <- index_iota a b | P x] idx
    have EX : exists k, b - a <= k.
x, a, b, idx: nat
P: nat -> bool
exists k : nat, b - a <= k
x, a, b, idx: nat
P: nat -> bool
EX: exists k : nat, b - a <= k
x < a ->
idx < size [seq x <- index_iota a b | P x] ->
x < nth 0 [seq x <- index_iota a b | P x] idx
    {
x, a, b, idx: nat
P: nat -> bool
exists k : nat, b - a <= k exists (b-a); by simpl. }
x, a, b, idx: nat
P: nat -> bool
EX: exists k : nat, b - a <= k
x < a ->
idx < size [seq x <- index_iota a b | P x] ->
x < nth 0 [seq x <- index_iota a b | P x] idx destruct EX as [k BO].
x, a, b, idx: nat
P: nat -> bool
k: nat
BO: b - a <= k
x < a ->
idx < size [seq x <- index_iota a b | P x] ->
x < nth 0 [seq x <- index_iota a b | P x] idx
    revert x a b idx P BO; elim: k => [|k IHk].
forall (x a b idx : nat) (P : nat -> bool),
b - a <= 0 ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
k: nat
IHk: forall (x a b idx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
forall (x a b idx : nat) (P : nat -> bool),
b - a <= k.+1 ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
    -
forall (x a b idx : nat) (P : nat -> bool),
b - a <= 0 ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx move => x a b idx P BO LT1 LT2.
x, a, b, idx: nat
P: nat -> bool
BO: b - a <= 0
LT1: x < a
LT2: idx < size [seq x <- index_iota a b | P x]
x < nth 0 [seq x <- index_iota a b | P x] idx
      move: BO; rewrite leqn0; move => /eqP BO.
x, a, b, idx: nat
P: nat -> bool
LT1: x < a
LT2: idx < size [seq x <- index_iota a b | P x]
BO: b - a = 0
x < nth 0 [seq x <- index_iota a b | P x] idx
        by rewrite /index_iota BO in LT2; simpl in LT2.
    -
k: nat
IHk: forall (x a b idx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
forall (x a b idx : nat) (P : nat -> bool),
b - a <= k.+1 ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx move => x a b idx P BO LT1 LT2.
k: nat
IHk: forall (x a b idx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
x, a, b, idx: nat
P: nat -> bool
BO: b - a <= k.+1
LT1: x < a
LT2: idx < size [seq x <- index_iota a b | P x]
x < nth 0 [seq x <- index_iota a b | P x] idx
      case: (leqP b a) => [N|N].
k: nat
IHk: forall (x a b idx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
x, a, b, idx: nat
P: nat -> bool
BO: b - a <= k.+1
LT1: x < a
LT2: idx < size [seq x <- index_iota a b | P x]
N: b <= a
x < nth 0 [seq x <- index_iota a b | P x] idx
k: nat
IHk: forall (x a b idx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
x, a, b, idx: nat
P: nat -> bool
BO: b - a <= k.+1
LT1: x < a
LT2: idx < size [seq x <- index_iota a b | P x]
N: a < b
x < nth 0 [seq x <- index_iota a b | P x] idx
      +
k: nat
IHk: forall (x a b idx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
x, a, b, idx: nat
P: nat -> bool
BO: b - a <= k.+1
LT1: x < a
LT2: idx < size [seq x <- index_iota a b | P x]
N: b <= a
x < nth 0 [seq x <- index_iota a b | P x] idx move: N; rewrite -subn_eq0; move => /eqP EQ.
k: nat
IHk: forall (x a b idx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
x, a, b, idx: nat
P: nat -> bool
BO: b - a <= k.+1
LT1: x < a
LT2: idx < size [seq x <- index_iota a b | P x]
EQ: b - a = 0
x < nth 0 [seq x <- index_iota a b | P x] idx
          by rewrite /index_iota EQ //= in LT2.
      +
k: nat
IHk: forall (x a b idx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
x, a, b, idx: nat
P: nat -> bool
BO: b - a <= k.+1
LT1: x < a
LT2: idx < size [seq x <- index_iota a b | P x]
N: a < b
x < nth 0 [seq x <- index_iota a b | P x] idx rewrite index_iota_lt_step; last by done.
k: nat
IHk: forall (x a b idx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
x, a, b, idx: nat
P: nat -> bool
BO: b - a <= k.+1
LT1: x < a
LT2: idx < size [seq x <- index_iota a b | P x]
N: a < b
x < nth 0 [seq x <- a :: index_iota a.+1 b | P x] idx
        simpl in *; destruct (P a) eqn:PA.
k: nat
IHk: forall (x a b idx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
x, a, b, idx: nat
P: nat -> bool
BO: b - a <= k.+1
LT1: x < a
LT2: idx < size [seq x <- index_iota a b | P x]
N: a < b
PA: P a = true
x <
nth 0 (a :: [seq x <- index_iota a.+1 b | P x]) idx
k: nat
IHk: forall (x a b idx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
x, a, b, idx: nat
P: nat -> bool
BO: b - a <= k.+1
LT1: x < a
LT2: idx < size [seq x <- index_iota a b | P x]
N: a < b
PA: P a = false
x < nth 0 [seq x <- index_iota a.+1 b | P x] idx
        *
k: nat
IHk: forall (x a b idx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
x, a, b, idx: nat
P: nat -> bool
BO: b - a <= k.+1
LT1: x < a
LT2: idx < size [seq x <- index_iota a b | P x]
N: a < b
PA: P a = true
x <
nth 0 (a :: [seq x <- index_iota a.+1 b | P x]) idx destruct idx; simpl; first by done.
k: nat
IHk: forall (x a b idx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
x, a, b, idx: nat
P: nat -> bool
BO: b - a <= k.+1
LT1: x < a
LT2: idx.+1 < size [seq x <- index_iota a b | P x]
N: a < b
PA: P a = true
x < nth 0 [seq x <- index_iota a.+1 b | P x] idx
          apply IHk; try lia.
k: nat
IHk: forall (x a b idx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
x, a, b, idx: nat
P: nat -> bool
BO: b - a <= k.+1
LT1: x < a
LT2: idx.+1 < size [seq x <- index_iota a b | P x]
N: a < b
PA: P a = true
idx < size [seq x <- index_iota a.+1 b | P x]
            by rewrite index_iota_lt_step // //= PA //= in LT2.
        *
k: nat
IHk: forall (x a b idx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
x, a, b, idx: nat
P: nat -> bool
BO: b - a <= k.+1
LT1: x < a
LT2: idx < size [seq x <- index_iota a b | P x]
N: a < b
PA: P a = false
x < nth 0 [seq x <- index_iota a.+1 b | P x] idx apply IHk; try lia.
k: nat
IHk: forall (x a b idx : nat) (P : nat -> bool),
b - a <= k ->
x < a ->
idx < size [seq x0 <- index_iota a b | P x0] ->
x < nth 0 [seq x0 <- index_iota a b | P x0] idx
x, a, b, idx: nat
P: nat -> bool
BO: b - a <= k.+1
LT1: x < a
LT2: idx < size [seq x <- index_iota a b | P x]
N: a < b
PA: P a = false
idx < size [seq x <- index_iota a.+1 b | P x]
            by rewrite index_iota_lt_step // //= PA //= in LT2.
  Qed.

End IotaRange.

(** A sequence [xs] is a prefix of another sequence [ys] iff
    there exists a sequence [xs_tail] such that [ys] is a
    concatenation of [xs] and [xs_tail]. *)
Definition prefix_of {T : eqType} (xs ys : seq T) := exists xs_tail, xs ++ xs_tail = ys.

(** Furthermore, every prefix of a sequence is said to be
    strict if it is not equal to the sequence itself. *)
Definition strict_prefix_of {T : eqType} (xs ys : seq T) :=
  exists xs_tail, xs_tail <> [::] /\ xs ++ xs_tail = ys.

(** We define a helper function that shifts a sequence of numbers forward
    by a constant offset, and an analogous version that shifts them backwards,
    removing any number that, in the absence of Coq' s saturating subtraction,
    would become negative. These functions are very useful in transforming
    abstract RTA's search space. *)
Definition shift_points_pos (xs : seq nat) (s : nat) : seq nat :=
  map (addn s) xs.
Definition shift_points_neg (xs : seq nat) (s : nat) : seq nat :=
  let nonsmall := filter (fun x => x >= s) xs in
  map (fun x => x - s) nonsmall.