Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
Require Export mathcomp.zify.zify. 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]. *)

forall (x : nat) (xs : seq nat), xs <> [::] -> last0 (x :: xs) = last0 xs

forall (x : nat) (xs : seq nat), xs <> [::] -> last0 (x :: xs) = last0 xs
by induction xs; last unfold last0. 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]. *)

forall xs_l xs_r : seq nat, 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
a: nat
xs_l: seq nat
IHxs_l: forall xs_r : seq nat, xs_r <> [::] -> last0 (xs_l ++ xs_r) = last0 xs_r
xs_r: seq nat
NEQ: xs_r <> [::]

last0 ((a :: xs_l) ++ xs_r) = last0 xs_r
a: nat
xs_l: seq nat
IHxs_l: forall xs_r : seq nat, xs_r <> [::] -> last0 (xs_l ++ xs_r) = last0 xs_r
xs_r: seq nat
NEQ: xs_r <> [::]

last0 (xs_l ++ xs_r) = last0 xs_r
a: nat
xs_l: seq nat
IHxs_l: forall xs_r : seq nat, xs_r <> [::] -> last0 (xs_l ++ xs_r) = last0 xs_r
xs_r: seq nat
NEQ: xs_r <> [::]
xs_l ++ xs_r <> [::]
a: nat
xs_l: seq nat
IHxs_l: forall xs_r : seq nat, xs_r <> [::] -> last0 (xs_l ++ xs_r) = last0 xs_r
xs_r: seq nat
NEQ: xs_r <> [::]

last0 (xs_l ++ xs_r) = last0 xs_r
a: nat
xs_l: seq nat
IHxs_l: forall xs_r : seq nat, xs_r <> [::] -> last0 (xs_l ++ xs_r) = last0 xs_r
xs_r: seq nat
NEQ: xs_r <> [::]
xs_l ++ xs_r <> [::]
a: nat
xs_l: seq nat
IHxs_l: forall xs_r : seq nat, xs_r <> [::] -> last0 (xs_l ++ xs_r) = last0 xs_r
xs_r: seq nat
NEQ: xs_r <> [::]

xs_l ++ xs_r <> [::]
a: nat
xs_l: seq nat
IHxs_l: forall xs_r : seq nat, xs_r <> [::] -> last0 (xs_l ++ xs_r) = last0 xs_r
xs_r: seq nat
NEQ: xs_r <> [::]

xs_l ++ xs_r <> [::]
by intros C; apply: NEQ; destruct xs_l. Qed. (** We also prove that [last0 xs = xs [| size xs -1 |] ]. *)

forall xs : seq nat, last0 xs = nth 0 xs (size xs).-1

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]]. *)

forall (x : nat) (xs : seq nat), xs <> [::] -> last0 xs = x -> exists xsh : seq nat, xsh ++ [:: x] = xs

forall (x : nat) (xs : seq nat), xs <> [::] -> last0 xs = x -> exists xsh : seq nat, xsh ++ [:: x] = xs
x: nat
xs: seq nat
NEQ: xs <> [::]
LAST: last0 xs = x

exists xsh : seq nat, xsh ++ [:: x] = xs
x, a: nat
xs: seq nat
NEQ: a :: xs <> [::]
LAST: last0 (a :: xs) = x
IHxs: xs <> [::] -> last0 xs = x -> exists xsh : seq nat, xsh ++ [:: x] = xs

exists xsh : seq nat, xsh ++ [:: x] = a :: xs
x, a: nat
NEQ: [:: a] <> [::]
LAST: last0 [:: a] = x
IHxs: [::] <> [::] -> last0 [::] = x -> exists xsh : seq nat, xsh ++ [:: x] = [::]

exists xsh : seq nat, xsh ++ [:: x] = [:: a]
x, a, n: nat
xs: seq nat
NEQ: [:: a, n & xs] <> [::]
LAST: last0 [:: a, n & xs] = x
IHxs: n :: xs <> [::] -> last0 (n :: xs) = x -> exists xsh : seq nat, xsh ++ [:: x] = n :: xs
exists xsh : seq nat, xsh ++ [:: x] = [:: a, n & xs]
x, a: nat
NEQ: [:: a] <> [::]
LAST: last0 [:: a] = x
IHxs: [::] <> [::] -> last0 [::] = x -> exists xsh : seq nat, xsh ++ [:: x] = [::]

exists xsh : seq nat, xsh ++ [:: x] = [:: a]
x, a, n: nat
xs: seq nat
NEQ: [:: a, n & xs] <> [::]
LAST: last0 [:: a, n & xs] = x
IHxs: n :: xs <> [::] -> last0 (n :: xs) = x -> exists xsh : seq nat, xsh ++ [:: x] = n :: xs
exists xsh : seq nat, xsh ++ [:: x] = [:: a, n & xs]
x, a, n: nat
xs: seq nat
NEQ: [:: a, n & xs] <> [::]
LAST: last0 [:: a, n & xs] = x
IHxs: n :: xs <> [::] -> last0 (n :: xs) = x -> exists xsh : seq nat, xsh ++ [:: x] = n :: xs

exists xsh : seq nat, xsh ++ [:: x] = [:: a, n & xs]
x, a, n: nat
xs: seq nat
NEQ: [:: a, n & xs] <> [::]
LAST: last0 [:: a, n & xs] = x
IHxs: n :: xs <> [::] -> last0 (n :: xs) = x -> exists xsh : seq nat, xsh ++ [:: x] = n :: xs

exists xsh : seq nat, xsh ++ [:: x] = [:: a, n & xs]
x, a, n: nat
xs: seq nat
NEQ: [:: a, n & xs] <> [::]
LAST: last0 [:: a, n & xs] = x
IHxs: exists xsh : seq nat, xsh ++ [:: x] = n :: xs

exists xsh : seq nat, xsh ++ [:: x] = [:: a, n & xs]
x, a, n: nat
xs: seq nat
NEQ: [:: a, n & xs] <> [::]
LAST: last0 [:: a, n & xs] = x
xsh: seq nat
EQ: xsh ++ [:: x] = n :: xs

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. *)

forall (x : nat) (xs : seq nat) (P : nat -> bool), xs <> [::] -> last0 xs = x -> P x -> last0 [seq x0 <- xs | P x0] = x

forall (x : nat) (xs : seq nat) (P : nat -> bool), xs <> [::] -> last0 xs = x -> P x -> last0 [seq x0 <- xs | P x0] = x
x: nat
xs: seq nat
P: nat -> bool
NEQ: xs <> [::]
LAST: last0 xs = x
PX: P x

last0 [seq x <- xs | P x] = x
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
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}]. *)

forall (x : nat) (xs : seq nat), max0 (x :: xs) = maxn x (max0 xs)

forall (x : nat) (xs : seq nat), max0 (x :: xs) = maxn x (max0 xs)

forall (xs : seq nat) (s x : nat), foldl maxn s (x :: xs) = maxn x (foldl maxn s xs)
L: forall (xs : seq nat) (s x : nat), foldl maxn s (x :: xs) = maxn x (foldl maxn s xs)
forall (x : nat) (xs : seq nat), max0 (x :: xs) = maxn x (max0 xs)

forall (xs : seq nat) (s x : nat), foldl maxn s (x :: xs) = maxn x (foldl maxn s xs)
s, x: nat

foldl maxn s [:: x] = maxn x (foldl maxn s [::])
a: nat
xs: seq nat
IHxs: forall s x : nat, foldl maxn s (x :: xs) = maxn x (foldl maxn s xs)
s, x: nat
foldl maxn s [:: x, a & xs] = maxn x (foldl maxn s (a :: xs))
s, x: nat

foldl maxn s [:: x] = maxn x (foldl maxn s [::])
a: nat
xs: seq nat
IHxs: forall s x : nat, foldl maxn s (x :: xs) = maxn x (foldl maxn s xs)
s, x: nat
foldl maxn s [:: x, a & xs] = maxn x (foldl maxn s (a :: xs))
a: nat
xs: seq nat
IHxs: forall s x : nat, foldl maxn s (x :: xs) = maxn x (foldl maxn s xs)
s, x: nat

foldl maxn s [:: x, a & xs] = maxn x (foldl maxn s (a :: xs))
a: nat
xs: seq nat
IHxs: forall s x : nat, foldl maxn s (x :: xs) = maxn x (foldl maxn s xs)
s, x: nat

foldl maxn s [:: x, a & xs] = maxn x (foldl maxn s (a :: xs))
by rewrite //= in IHxs; rewrite //= maxnC IHxs [maxn s a]maxnC IHxs maxnA [maxn s x]maxnC.
L: forall (xs : seq nat) (s x : nat), foldl maxn s (x :: xs) = maxn x (foldl maxn s xs)

forall (x : nat) (xs : seq nat), max0 (x :: xs) = maxn x (max0 xs)
by intros; unfold max; apply L. Qed. (** Next, we prove that if all the numbers of a seq [xs] are equal to a constant [k], then [max0 xs = k]. *)

forall (k : nat_eqType) (xs : seq nat_eqType), 0 < size xs -> (forall x : nat_eqType, x \in xs -> x = k) -> max0 xs = k

forall (k : nat_eqType) (xs : seq nat_eqType), 0 < size xs -> (forall x : nat_eqType, x \in xs -> x = k) -> max0 xs = k
k: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size xs
ALL: forall x : nat_eqType, x \in xs -> x = k

max0 xs = k
k, a: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size (a :: xs)
ALL: forall x : nat_eqType, x \in a :: xs -> x = k
IHxs: 0 < size xs -> (forall x : nat_eqType, x \in xs -> x = k) -> max0 xs = k

max0 (a :: xs) = k
k, a: nat_eqType
SIZE: 0 < size [:: a]
ALL: forall x : nat_eqType, x \in [:: a] -> x = k
IHxs: 0 < size [::] -> (forall x : nat_eqType, x \in [::] -> x = k) -> max0 [::] = k

max0 [:: a] = k
k, a, s: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size [:: a, s & xs]
ALL: forall x : nat_eqType, x \in [:: a, s & xs] -> x = k
IHxs: 0 < size (s :: xs) -> (forall x : nat_eqType, x \in s :: xs -> x = k) -> max0 (s :: xs) = k
max0 [:: a, s & xs] = k
k, a: nat_eqType
SIZE: 0 < size [:: a]
ALL: forall x : nat_eqType, x \in [:: a] -> x = k
IHxs: 0 < size [::] -> (forall x : nat_eqType, x \in [::] -> x = k) -> max0 [::] = k

max0 [:: a] = k
k, a, s: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size [:: a, s & xs]
ALL: forall x : nat_eqType, x \in [:: a, s & xs] -> x = k
IHxs: 0 < size (s :: xs) -> (forall x : nat_eqType, x \in s :: xs -> x = k) -> max0 (s :: xs) = k
max0 [:: a, s & xs] = k
k, a: nat_eqType
SIZE: 0 < size [:: a]
ALL: forall x : nat_eqType, x \in [:: a] -> x = k
IHxs: 0 < size [::] -> (forall x : nat_eqType, x \in [::] -> x = k) -> max0 [::] = k

a \in [:: a]
k, a, s: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size [:: a, s & xs]
ALL: forall x : nat_eqType, x \in [:: a, s & xs] -> x = k
IHxs: 0 < size (s :: xs) -> (forall x : nat_eqType, x \in s :: xs -> x = k) -> max0 (s :: xs) = k
max0 [:: a, s & xs] = k
k, a, s: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size [:: a, s & xs]
ALL: forall x : nat_eqType, x \in [:: a, s & xs] -> x = k
IHxs: 0 < size (s :: xs) -> (forall x : nat_eqType, x \in s :: xs -> x = k) -> max0 (s :: xs) = k

max0 [:: a, s & xs] = k
k, a, s: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size [:: a, s & xs]
ALL: forall x : nat_eqType, x \in [:: a, s & xs] -> x = k
IHxs: 0 < size (s :: xs) -> (forall x : nat_eqType, x \in s :: xs -> x = k) -> max0 (s :: xs) = k

max0 [:: a, s & xs] = k
k, a, s: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size [:: a, s & xs]
ALL: forall x : nat_eqType, x \in [:: a, s & xs] -> x = k
IHxs: 0 < size (s :: xs) -> (forall x : nat_eqType, x \in s :: xs -> x = k) -> max0 (s :: xs) = k

maxn a k = k
k, a, s: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size [:: a, s & xs]
ALL: forall x : nat_eqType, x \in [:: a, s & xs] -> x = k
IHxs: 0 < size (s :: xs) -> (forall x : nat_eqType, x \in s :: xs -> x = k) -> max0 (s :: xs) = k
forall x : nat_eqType, x \in s :: xs -> x = k
k, a, s: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size [:: a, s & xs]
ALL: forall x : nat_eqType, x \in [:: a, s & xs] -> x = k
IHxs: 0 < size (s :: xs) -> (forall x : nat_eqType, x \in s :: xs -> x = k) -> max0 (s :: xs) = k

maxn a k = k
k, a, s: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size [:: a, s & xs]
ALL: forall x : nat_eqType, x \in [:: a, s & xs] -> x = k
IHxs: 0 < size (s :: xs) -> (forall x : nat_eqType, x \in s :: xs -> x = k) -> max0 (s :: xs) = k
forall x : nat_eqType, x \in s :: xs -> x = k
k, a, s: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size [:: a, s & xs]
ALL: forall x : nat_eqType, x \in [:: a, s & xs] -> x = k
IHxs: 0 < size (s :: xs) -> (forall x : nat_eqType, x \in s :: xs -> x = k) -> max0 (s :: xs) = k

forall x : nat_eqType, x \in s :: xs -> x = k
k, a, s: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size [:: a, s & xs]
ALL: forall x : nat_eqType, x \in [:: a, s & xs] -> x = k
IHxs: 0 < size (s :: xs) -> (forall x : nat_eqType, x \in s :: xs -> x = k) -> max0 (s :: xs) = k

forall x : nat_eqType, x \in s :: xs -> x = k
k, a, s: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size [:: a, s & xs]
ALL: forall x : nat_eqType, x \in [:: a, s & xs] -> x = k
IHxs: 0 < size (s :: xs) -> (forall x : nat_eqType, x \in s :: xs -> x = k) -> max0 (s :: xs) = k
x: nat_eqType
H: x \in s :: xs

x \in [:: a, s & xs]
k, a, s: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size [:: a, s & xs]
ALL: forall x : nat_eqType, x \in [:: a, s & xs] -> x = k
IHxs: 0 < size (s :: xs) -> (forall x : nat_eqType, x \in s :: xs -> x = k) -> max0 (s :: xs) = k
x: nat_eqType
EQ: x = s

x \in [:: a, s & xs]
k, a, s: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size [:: a, s & xs]
ALL: forall x : nat_eqType, x \in [:: a, s & xs] -> x = k
IHxs: 0 < size (s :: xs) -> (forall x : nat_eqType, x \in s :: xs -> x = k) -> max0 (s :: xs) = k
x: nat_eqType
IN: x \in xs
x \in [:: a, s & xs]
k, a, s: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size [:: a, s & xs]
ALL: forall x : nat_eqType, x \in [:: a, s & xs] -> x = k
IHxs: 0 < size (s :: xs) -> (forall x : nat_eqType, x \in s :: xs -> x = k) -> max0 (s :: xs) = k
x: nat_eqType
EQ: x = s

x \in [:: a, s & xs]
k, a, s: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size [:: a, s & xs]
ALL: forall x : nat_eqType, x \in [:: a, s & xs] -> x = k
IHxs: 0 < size (s :: xs) -> (forall x : nat_eqType, x \in s :: xs -> x = k) -> max0 (s :: xs) = k
x: nat_eqType
IN: x \in xs
x \in [:: a, s & xs]
k, a, s: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size [:: a, s & xs]
ALL: forall x : nat_eqType, x \in [:: a, s & xs] -> x = k
IHxs: 0 < size (s :: xs) -> (forall x : nat_eqType, x \in s :: xs -> x = k) -> max0 (s :: xs) = k
x: nat_eqType
IN: x \in xs

x \in [:: a, s & xs]
k, a, s: nat_eqType
xs: seq nat_eqType
SIZE: 0 < size [:: a, s & xs]
ALL: forall x : nat_eqType, x \in [:: a, s & xs] -> x = k
IHxs: 0 < size (s :: xs) -> (forall x : nat_eqType, x \in s :: xs -> x = k) -> max0 (s :: xs) = k
x: nat_eqType
IN: x \in xs

x \in [:: a, s & 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]. *)

forall (xs : seq_predType nat_eqType) (x : nat), x \in xs -> x <= max0 xs

forall (xs : seq_predType nat_eqType) (x : nat), x \in xs -> x <= max0 xs
a: nat_eqType
xs: seq nat_eqType
IHxs: forall x : nat, x \in xs -> x <= max0 xs

forall x : nat, x \in a :: xs -> x <= max0 (a :: xs)
a: nat_eqType
xs: seq nat_eqType
IHxs: forall x : nat, x \in xs -> x <= max0 xs

a <= max0 (a :: xs)
a: nat_eqType
xs: seq nat_eqType
IHxs: forall x : nat, x \in xs -> x <= max0 xs
x: nat
IN: x \in xs
x <= max0 (a :: xs)
a: nat_eqType
xs: seq nat_eqType
IHxs: forall x : nat, x \in xs -> x <= max0 xs

a <= max0 (a :: xs)
a: nat_eqType
xs: seq nat_eqType
IHxs: forall x : nat, x \in xs -> x <= max0 xs
x: nat
IN: x \in xs
x <= max0 (a :: xs)
a: nat_eqType
xs: seq nat_eqType
IHxs: forall x : nat, x \in xs -> x <= max0 xs
x: nat
IN: x \in xs

x <= max0 (a :: xs)
a: nat_eqType
xs: seq nat_eqType
IHxs: forall x : nat, x \in xs -> x <= max0 xs
x: nat
IN: x \in xs

x <= max0 (a :: xs)
a: nat_eqType
xs: seq nat_eqType
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]. *)

forall xs : seq nat, xs <> [::] -> max0 xs \in xs

forall xs : seq nat, xs <> [::] -> max0 xs \in xs
a: nat
xs: seq nat
IHxs: xs <> [::] -> max0 xs \in xs

a :: xs <> [::] -> max0 (a :: xs) \in a :: 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]
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.+1] \in [:: a.+1]
a, n: nat
xs: seq nat
IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
max0 [:: a, n & xs] \in [:: a, n & xs]
a, n: nat
xs: seq nat
IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs

max0 [:: a, n & xs] \in [:: a, n & xs]
a, n: nat
xs: seq nat
IHxs: n :: xs <> [::] -> max0 (n :: xs) \in n :: xs

max0 [:: a, n & xs] \in [:: a, n & xs]
a, n: nat
xs: seq nat
IHxs: n :: xs <> [::] -> max0 (n :: xs) \in 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: 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]
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: 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: 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
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. *)

forall (x : nat) (xs : seq nat), max0 [:: x, x & xs] = max0 (x :: xs)

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. *)

forall (x1 x2 : nat) (xs : seq nat), 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)
by intros; 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. *)

forall xs : seq nat, max0 [seq x <- xs | 0 < x] = max0 xs

forall xs : seq nat, max0 [seq x <- xs | 0 < x] = max0 xs
a: nat
xs: seq nat
IHxs: max0 [seq x <- xs | 0 < x] = max0 xs

max0 [seq x <- a :: xs | 0 < x] = max0 (a :: xs)
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)
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)
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)
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. *)

forall xs : seq nat, last0 xs <= max0 xs

forall xs : seq nat, last0 xs <= max0 xs
xs: seq nat

last0 xs <= max0 xs
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
xs: seq nat
len: nat
LE: size xs <= len

last0 xs <= max0 xs

forall xs : seq nat, size xs <= 0 -> last0 xs <= max0 xs
len: nat
IHlen: forall xs : seq nat, size xs <= len -> last0 xs <= max0 xs
forall xs : seq nat, size xs <= len.+1 -> last0 xs <= max0 xs

forall xs : seq nat, size xs <= 0 -> last0 xs <= max0 xs
len: nat
IHlen: forall xs : seq nat, size xs <= len -> last0 xs <= max0 xs
forall xs : seq nat, size xs <= len.+1 -> last0 xs <= max0 xs
len: nat
IHlen: forall xs : seq nat, size xs <= len -> last0 xs <= max0 xs

forall xs : seq nat, size xs <= len.+1 -> last0 xs <= max0 xs
len: nat
IHlen: forall xs : seq nat, size xs <= len -> last0 xs <= max0 xs

forall xs : seq nat, size xs <= len.+1 -> last0 xs <= max0 xs
len: nat
IHlen: forall xs : seq nat, size xs <= len -> last0 xs <= max0 xs
xs: seq nat
SIZE: size xs <= len.+1

last0 xs <= max0 xs
len: nat
IHlen: forall xs : seq nat, size xs <= len -> last0 xs <= max0 xs
xs: seq nat
EQ: size xs = len.+1

last0 xs <= max0 xs
len: nat
IHlen: forall xs : seq nat, size xs <= len -> last0 xs <= max0 xs
x1: nat
xs: seq nat
EQ: size (x1 :: xs) = len.+1

last0 (x1 :: xs) <= max0 (x1 :: xs)
len: nat
IHlen: forall xs : seq nat, size xs <= len -> last0 xs <= max0 xs
x1, x2: nat
xs: seq nat
EQ: size [:: x1, x2 & xs] = len.+1

last0 [:: x1, x2 & xs] <= max0 [:: x1, x2 & xs]
len: nat
IHlen: forall xs : seq nat, size xs <= len -> last0 xs <= max0 xs
x1, x2: nat
xs: seq nat
EQ: size [:: x1, x2 & xs] = len.+1

last0 (x2 :: xs) <= max0 [:: x1, x2 & xs]
len: nat
IHlen: forall xs : seq nat, size xs <= len -> last0 xs <= max0 xs
x1, x2: nat
xs: seq nat
EQ: size [:: x1, x2 & xs] = len.+1

size (x2 :: xs) <= len
len: nat
IHlen: forall xs : seq nat, size xs <= len -> last0 xs <= max0 xs
x1, x2: nat
xs: seq nat
EQ: (size xs).+1 = len

size xs < len
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]. *)

forall xs ys : seq nat, (forall n : nat, xs [|n|] <= ys [|n|]) -> max0 xs <= max0 ys

forall xs ys : seq nat, (forall n : nat, xs [|n|] <= ys [|n|]) -> max0 xs <= max0 ys
xs, ys: seq nat

(forall n : nat, xs [|n|] <= ys [|n|]) -> max0 xs <= max0 ys
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
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
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
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
ys: seq nat
LE2: size ys <= 0
xs: seq nat
LE1: size xs <= 0
H: forall n : nat, xs [|n|] <= ys [|n|]

max0 xs <= max0 ys
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
ys: seq nat
LE2: size ys <= len.+1
xs: seq nat
LE1: size xs <= len.+1
H: forall n : nat, xs [|n|] <= ys [|n|]
max0 xs <= max0 ys
ys: seq nat
LE2: size ys <= 0
xs: seq nat
LE1: size xs <= 0
H: forall n : nat, xs [|n|] <= ys [|n|]

max0 xs <= max0 ys
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
ys: seq nat
LE2: size ys <= len.+1
xs: seq nat
LE1: size xs <= len.+1
H: forall n : nat, xs [|n|] <= ys [|n|]

max0 xs <= max0 ys
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
ys: seq nat
LE2: size ys <= len.+1
xs: seq nat
LE1: size xs <= len.+1
H: forall n : nat, xs [|n|] <= ys [|n|]

max0 xs <= max0 ys
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
LE2: size [::] <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n0 : nat, (n :: xs) [|n0|] <= [::] [|n0|]

max0 (n :: xs) <= 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
n0: nat
ys: seq nat
LE2: size (n0 :: ys) <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n1 : nat, (n :: xs) [|n1|] <= (n0 :: ys) [|n1|]
max0 (n :: xs) <= max0 (n0 :: ys)
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
LE2: size [::] <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n0 : nat, (n :: xs) [|n0|] <= [::] [|n0|]

max0 (n :: xs) <= 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
LE2: size [::] <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n0 : nat, (n :: xs) [|n0|] <= [::] [|n0|]

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
LE2: size [::] <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n0 : nat, (n :: xs) [|n0|] <= [::] [|n0|]
L: forall xs : seq nat, (forall n : nat, xs [|n|] = 0) -> max0 xs = 0
max0 (n :: xs) <= 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
LE2: size [::] <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n0 : nat, (n :: xs) [|n0|] <= [::] [|n0|]

forall xs : seq nat, (forall n : nat, xs [|n|] = 0) -> max0 xs = 0
xs: seq nat
H: forall n : nat, xs [|n|] = 0

max0 xs = 0
a: nat
xs: seq nat
H: forall n : nat, (a :: xs) [|n|] = 0
IHxs: (forall n : nat, xs [|n|] = 0) -> max0 xs = 0

max0 (a :: xs) = 0
a: nat
xs: seq nat
H: forall n : nat, (a :: xs) [|n|] = 0
IHxs: (forall n : nat, xs [|n|] = 0) -> max0 xs = 0

maxn a (max0 xs) = 0
a: nat
xs: seq nat
H: forall n : nat, (a :: xs) [|n|] = 0
IHxs: (forall n : nat, xs [|n|] = 0) -> max0 xs = 0

maxn a (max0 xs) <= 0
a: nat
xs: seq nat
H: forall n : nat, (a :: xs) [|n|] = 0
IHxs: (forall n : nat, xs [|n|] = 0) -> max0 xs = 0

a <= 0
a: nat
xs: seq nat
H: forall n : nat, (a :: xs) [|n|] = 0
IHxs: (forall n : nat, xs [|n|] = 0) -> max0 xs = 0
max0 xs <= 0
a: nat
xs: seq nat
H: forall n : nat, (a :: xs) [|n|] = 0
IHxs: (forall n : nat, xs [|n|] = 0) -> max0 xs = 0

a <= 0
a: nat
xs: seq nat
H: forall n : nat, (a :: xs) [|n|] = 0
IHxs: (forall n : nat, xs [|n|] = 0) -> max0 xs = 0
max0 xs <= 0
a: nat
xs: seq nat
H: forall n : nat, (a :: xs) [|n|] = 0
IHxs: (forall n : nat, xs [|n|] = 0) -> max0 xs = 0

max0 xs <= 0
a: nat
xs: seq nat
H: forall n : nat, (a :: xs) [|n|] = 0
IHxs: (forall n : nat, xs [|n|] = 0) -> max0 xs = 0

max0 xs <= 0
a: nat
xs: seq nat
H: forall n : nat, (a :: xs) [|n|] = 0

forall n : nat, xs [|n|] = 0
by intros; 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
LE2: size [::] <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n0 : nat, (n :: xs) [|n0|] <= [::] [|n0|]
L: forall xs : seq nat, (forall n : nat, xs [|n|] = 0) -> max0 xs = 0

max0 (n :: xs) <= 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
LE2: size [::] <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n0 : nat, (n :: xs) [|n0|] <= [::] [|n0|]
L: forall xs : seq nat, (forall n : nat, xs [|n|] = 0) -> max0 xs = 0

forall n0 : nat, (n :: xs) [|n0|] = 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
LE2: size [::] <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
n0: nat
H: (n :: xs) [|n0|] <= [::] [|n0|]
L: forall xs : seq nat, (forall n : nat, xs [|n|] = 0) -> max0 xs = 0

(n :: xs) [|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
n0: nat
ys: seq nat
LE2: size (n0 :: ys) <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n1 : nat, (n :: xs) [|n1|] <= (n0 :: ys) [|n1|]

max0 (n :: xs) <= max0 (n0 :: ys)
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
n0: nat
ys: seq nat
LE2: size (n0 :: ys) <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n1 : nat, (n :: xs) [|n1|] <= (n0 :: ys) [|n1|]

max0 (n :: xs) <= max0 (n0 :: ys)
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
n0: nat
ys: seq nat
LE2: size (n0 :: ys) <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n1 : nat, (n :: xs) [|n1|] <= (n0 :: ys) [|n1|]

n <= maxn n0 (max0 ys)
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
n0: nat
ys: seq nat
LE2: size (n0 :: ys) <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n1 : nat, (n :: xs) [|n1|] <= (n0 :: ys) [|n1|]
max0 xs <= maxn n0 (max0 ys)
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
n0: nat
ys: seq nat
LE2: size (n0 :: ys) <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n1 : nat, (n :: xs) [|n1|] <= (n0 :: ys) [|n1|]

n <= maxn n0 (max0 ys)
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
n0: nat
ys: seq nat
LE2: size (n0 :: ys) <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n1 : nat, (n :: xs) [|n1|] <= (n0 :: ys) [|n1|]
max0 xs <= maxn n0 (max0 ys)
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
n0: nat
ys: seq nat
LE2: size (n0 :: ys) <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n1 : nat, (n :: xs) [|n1|] <= (n0 :: ys) [|n1|]

n <= 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
n0: nat
ys: seq nat
LE2: size (n0 :: ys) <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n1 : nat, (n :: xs) [|n1|] <= (n0 :: ys) [|n1|]
max0 xs <= maxn n0 (max0 ys)
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
n0: nat
ys: seq nat
LE2: size (n0 :: ys) <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n1 : nat, (n :: xs) [|n1|] <= (n0 :: ys) [|n1|]

max0 xs <= maxn n0 (max0 ys)
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
n0: nat
ys: seq nat
LE2: size (n0 :: ys) <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n1 : nat, (n :: xs) [|n1|] <= (n0 :: ys) [|n1|]

max0 xs <= maxn n0 (max0 ys)
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
n0: nat
ys: seq nat
LE2: size (n0 :: ys) <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n1 : nat, (n :: xs) [|n1|] <= (n0 :: ys) [|n1|]

max0 xs <= max0 ys
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
n0: nat
ys: seq nat
LE2: size (n0 :: ys) <= len.+1
n: nat
xs: seq nat
LE1: size (n :: xs) <= len.+1
H: forall n1 : nat, (n :: xs) [|n1|] <= (n0 :: ys) [|n1|]

forall n : nat, xs [|n|] <= ys [|n|]
by intros; 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]. *)

forall (X : eqType) (x y : X) (xs : seq X), x \in rem (T:=X) y xs -> x \in xs

forall (X : eqType) (x y : X) (xs : seq X), x \in rem (T:=X) y xs -> x \in xs
X: eqType
x, y: X
H: x \in [::]

x \in [::]
X: eqType
x, y, a: X
xs: seq X
H: x \in (if a == y then xs else a :: rem (T:=X) y xs)
IHxs: x \in rem (T:=X) y xs -> x \in 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
H: x \in (if a == y then xs else a :: rem (T:=X) y xs)
IHxs: x \in rem (T:=X) y xs -> x \in xs

x \in a :: xs
X: eqType
x, y, a: X
xs: seq X
H: x \in (if a == y then xs else a :: rem (T:=X) y xs)
IHxs: x \in rem (T:=X) y xs -> x \in xs

x \in a :: xs
X: eqType
x, y, a: X
xs: seq X
H: x \in (if a == y then xs else a :: rem (T:=X) y xs)
IHxs: x \in rem (T:=X) y xs -> x \in xs

x == a \/ x \in xs
X: eqType
x, y, a: X
xs: seq X
EQ: (a == y) = true
H: x \in xs
IHxs: x \in rem (T:=X) y xs -> x \in xs

x == a \/ x \in xs
X: eqType
x, y, a: X
xs: seq X
EQ: (a == y) = false
H: x \in a :: rem (T:=X) y xs
IHxs: x \in rem (T:=X) y xs -> x \in xs
x == a \/ x \in xs
X: eqType
x, y, a: X
xs: seq X
EQ: (a == y) = true
H: x \in xs
IHxs: x \in rem (T:=X) y xs -> 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
EQ: (a == y) = false
H: x \in a :: rem (T:=X) y xs
IHxs: x \in rem (T:=X) y xs -> x \in xs

x == a \/ x \in xs
X: eqType
x, y, a: X
xs: seq X
EQ: (a == y) = false
H: x \in a :: rem (T:=X) y xs
IHxs: x \in rem (T:=X) y xs -> x \in xs

x == a \/ x \in xs
X: eqType
x, y, a: X
xs: seq X
EQ: (a == y) = false
IHxs: x \in rem (T:=X) y xs -> x \in xs
H: x = a

x == a \/ x \in xs
X: eqType
x, y, a: X
xs: seq X
EQ: (a == y) = false
IHxs: x \in rem (T:=X) y xs -> x \in xs
H: x \in rem (T:=X) y xs
x == a \/ x \in xs
X: eqType
x, y, a: X
xs: seq X
EQ: (a == y) = false
IHxs: x \in rem (T:=X) y xs -> x \in xs
H: x = a

x == a \/ x \in xs
X: eqType
x, y, a: X
xs: seq X
EQ: (a == y) = false
IHxs: x \in rem (T:=X) y xs -> x \in xs
H: x \in rem (T:=X) y xs
x == a \/ x \in xs
X: eqType
x, y, a: X
xs: seq X
EQ: (a == y) = false
IHxs: x \in rem (T:=X) y xs -> x \in xs
H: x \in rem (T:=X) y xs

x == a \/ x \in xs
X: eqType
x, y, a: X
xs: seq X
EQ: (a == y) = false
IHxs: x \in rem (T:=X) y xs -> x \in xs
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]. *)

forall (X : eqType) (x y : X) (xs : seq X), x \in xs -> x != y -> x \in rem (T:=X) y xs

forall (X : eqType) (x y : X) (xs : seq X), x \in xs -> x != y -> x \in rem (T:=X) y xs
X: eqType
x, y: X

x \in [::] -> x != y -> x \in rem (T:=X) y [::]
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)
X: eqType
x, y: X

x \in [::] -> x != y -> x \in rem (T:=X) y [::]
intros ?; by done.
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)
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)
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)
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)
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)
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
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]. *)

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

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
X: eqType
x, a: X
xs: seq X
P: pred X
H: x \in a :: xs
H0: P x
IHxs: x \in xs -> size [seq y <- xs | P y] = size [seq y <- rem (T:=X) x xs | P y] + 1

size [seq y <- a :: xs | P y] = size [seq y <- rem (T:=X) x (a :: xs) | P y] + 1
X: eqType
a: X
xs: seq X
P: pred X
IHxs: a \in xs -> size [seq y <- xs | P y] = size [seq y <- rem (T:=X) a xs | P y] + 1
H0: P a

size [seq y <- a :: xs | P y] = size [seq y <- rem (T:=X) a (a :: xs) | P y] + 1
X: eqType
x, a: X
xs: seq X
P: pred X
H0: P 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
a: X
xs: seq X
P: pred X
IHxs: a \in xs -> size [seq y <- xs | P y] = size [seq y <- rem (T:=X) a xs | P y] + 1
H0: P a

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, a: X
xs: seq X
P: pred X
H0: P 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, a: X
xs: seq X
P: pred X
H0: P 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, a: X
xs: seq X
P: pred X
H0: P 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
X: eqType
x, a: X
xs: seq X
P: pred X
H0: P 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, a: X
xs: seq X
P: pred X
H0: P 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, a: X
xs: seq X
P: pred X
H0: P 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
xs: seq X
P: pred X
H0: P 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, a: X
xs: seq X
P: pred X
H0: P 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, a: X
xs: seq X
P: pred X
H0: P 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, a: X
xs: seq X
P: pred X
H0: P 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, a: X
xs: seq X
P: pred X
H0: P 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, a: X
xs: seq X
P: pred X
H0: P 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, a: X
xs: seq X
P: pred X
H0: P 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, a: X
xs: seq X
P: pred X
H0: P 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, a: X
xs: seq X
P: pred X
H0: P 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 prove that [x::xs = ys] is a sufficient condition for [x] to be in [ys]. *)

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
X: eqType
x: X
xs: seq X
y: X
ys: seq X
EQ: x :: xs = y :: ys

x \in y :: ys
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)]. *)

forall (x : nat) (xs : seq nat) (n : nat), 0 < n -> 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
by intros; destruct n. 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]]. *)

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

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
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
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
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
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
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
x: X
SIZE: size [:: x] = 1

exists (x0 : X) (xs__c : seq X), [:: x] = xs__c ++ [:: x0] /\ 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
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
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
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
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
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
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
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
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
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]]. *)

forall (X : eqType) (x : X) (xs : seq X), x \in xs -> exists xsl xsr : seq X, xs = xsl ++ [:: x] ++ xsr

forall (X : eqType) (x : X) (xs : seq X), x \in xs -> exists xsl xsr : seq X, xs = xsl ++ [:: x] ++ xsr
X: eqType
x: X
xs: seq X
SUB: x \in xs

exists xsl xsr : seq X, xs = xsl ++ [:: x] ++ xsr
X: eqType
x, a: X
xs: seq X
SUB: x \in a :: xs
IHxs: x \in xs -> exists xsl xsr : seq X, xs = xsl ++ [:: x] ++ xsr

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
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
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
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
IN: x \in xs

exists xsl xsr : seq X, a :: xs = xsl ++ [:: x] ++ xsr
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
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]. *)

forall (X : eqType) (xs ys : seq X), uniq xs -> (forall x : 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
X: eqType
xs, ys: seq X
UNIQ: uniq xs
SUB: forall x : X, x \in xs -> x \in ys

size xs <= 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
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
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
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
X: eqType
xs: seq X
UNIQ: uniq xs
SUB: forall x : X, x \in xs -> x \in [::]

size xs <= size [::]
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 [::]
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
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
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
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
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)
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
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
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
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

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

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

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

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
a: X
IN: a \in xs

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
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
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
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
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
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
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)
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 [:: 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 [:: 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 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 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]. *)

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

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
X, Y: eqType
x1: X
xs: seq X
IHxs: forall (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
ys: seq Y
x, x__d: X
y, y__d: 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
X, Y: eqType
x1: X
xs: seq X
IHxs: forall (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
y1: Y
ys: seq Y
x, x__d: X
y, y__d: 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)
X, Y: eqType
x1: X
xs: seq X
IHxs: forall (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
y1: Y
ys: seq Y
x, x__d: X
y, y__d: 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
X, Y: eqType
x1: X
xs: seq X
IHxs: forall (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
y1: Y
ys: seq Y
x, x__d: X
y, y__d: 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
x1: X
xs: seq X
IHxs: forall (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
y1: Y
ys: seq Y
x, x__d: X
y, y__d: 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
x1: X
xs: seq X
IHxs: forall (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
y1: Y
ys: seq Y
x, x__d: X
y, y__d: 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
x1: X
xs: seq X
IHxs: forall (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
y1: Y
ys: seq Y
x, x__d: X
y, y__d: 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
x1: X
xs: seq X
IHxs: forall (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
y1: Y
ys: seq Y
x, x__d: X
y, y__d: 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
x1: X
xs: seq X
IHxs: forall (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
y1: Y
ys: seq Y
x, x__d: X
y, y__d: 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
X, Y: eqType
x1: X
xs: seq X
IHxs: forall (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
y1: Y
ys: seq Y
x, x__d: X
y, y__d: 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
x1: X
xs: seq X
IHxs: forall (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
y1: Y
ys: seq Y
x, x__d: X
y, y__d: 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 idx0 : nat, idx0 < size xs /\ nth ?x__d xs idx0 = x /\ nth ?y__d ys idx0 = y
X, Y: eqType
x1: X
xs: seq X
IHxs: forall (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
y1: Y
ys: seq Y
x, x__d: X
y, y__d: 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
x1: X
xs: seq X
IHxs: forall (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
y1: Y
ys: seq Y
x, x__d: X
y, y__d: 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 idx0 : nat, idx0 < size xs /\ nth ?x__d xs idx0 = x /\ nth ?y__d ys idx0 = y
X, Y: eqType
x1: X
xs: seq X
IHxs: forall (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
y1: Y
ys: seq Y
x, x__d: X
y, y__d: 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 idx0 : nat, idx0 < size xs /\ nth ?x__d xs idx0 = x /\ nth ?y__d ys idx0 = y
X, Y: eqType
x1: X
xs: seq X
IHxs: forall (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
y1: Y
ys: seq Y
x, x__d: X
y, y__d: 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 idx0 : nat, idx0 < size xs /\ nth ?x__d xs idx0 = x /\ nth ?y__d ys idx0 = 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)]. *)

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

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
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
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
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
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
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
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)
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
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
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
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

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

nth ?x__d xs idx = x
by apply nth_index. -
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]. *)

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

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
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
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
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
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
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
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
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
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
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
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
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)
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
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
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 x :: 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
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 != 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
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
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
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. *)

forall (X : eqType) (xs : seq X) (P : pred X), (forall x : X, x \in xs -> ~~ P x) -> [seq x <- xs | P x] = [::]

forall (X : eqType) (xs : seq X) (P : pred X), (forall x : X, x \in xs -> ~~ P x) -> [seq x <- xs | P x] = [::]
X: eqType
xs: seq X
P: pred X
ALLF: forall x : X, x \in xs -> ~~ P x

[seq x <- xs | P x] = [::]
X: eqType
a: X
xs: seq X
P: pred X
ALLF: forall x : X, x \in a :: xs -> ~~ P x
IHxs: (forall x : X, x \in xs -> ~~ P x) -> [seq x <- xs | P x] = [::]

[seq x <- a :: xs | P x] = [::]
X: eqType
a: X
xs: seq X
P: pred X
ALLF: forall x : X, x \in a :: xs -> ~~ P x
IHxs: (forall x : X, x \in xs -> ~~ P x) -> [seq x <- xs | P x] = [::]

forall x : X, x \in xs -> ~~ P x
X: eqType
a: X
xs: seq X
P: pred X
ALLF: forall x : X, x \in a :: xs -> ~~ P x
IHxs: (forall x : X, x \in xs -> ~~ P x) -> [seq x <- xs | P x] = [::]
(if P a then [:: a] else [::]) = [::]
X: eqType
a: X
xs: seq X
P: pred X
ALLF: forall x : X, x \in a :: xs -> ~~ P x
IHxs: (forall x : X, x \in xs -> ~~ P x) -> [seq x <- xs | P x] = [::]

forall x : X, x \in xs -> ~~ P x
X: eqType
a: X
xs: seq X
P: pred X
ALLF: forall x : X, x \in a :: xs -> ~~ P x
IHxs: (forall x : X, x \in xs -> ~~ P x) -> [seq x <- xs | P x] = [::]
(if P a then [:: a] else [::]) = [::]
X: eqType
a: X
xs: seq X
P: pred X
ALLF: forall x : X, x \in a :: xs -> ~~ P x
IHxs: (forall x : X, x \in xs -> ~~ P x) -> [seq x <- xs | P x] = [::]

(if P a then [:: a] else [::]) = [::]
X: eqType
a: X
xs: seq X
P: pred X
ALLF: forall x : X, x \in a :: xs -> ~~ P x
IHxs: (forall x : X, x \in xs -> ~~ P x) -> [seq x <- xs | P x] = [::]

(if P a then [:: a] else [::]) = [::]
X: eqType
a: X
xs: seq X
P: pred X
ALLF: forall x : X, x \in a :: xs -> ~~ P x
IHxs: (forall x : X, x \in xs -> ~~ P x) -> [seq x <- xs | P x] = [::]
EQ: P a = true

[:: a] = [::]
X: eqType
a: X
xs: seq X
P: pred X
ALLF: forall x : X, x \in a :: xs -> ~~ P x
IHxs: (forall x : X, x \in xs -> ~~ P x) -> [seq x <- xs | P x] = [::]
T: ~ ~~ P a

[:: a] = [::]
X: eqType
a: X
xs: seq X
P: pred X
ALLF: forall x : X, x \in a :: xs -> ~~ P x
IHxs: (forall x : X, x \in xs -> ~~ P x) -> [seq x <- 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. *)

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
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
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
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. *)

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
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
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: n < size xs

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
by right; apply mem_nth. Qed. (** We show that in a unique sequence of size greater than one there exist two unique elements. *)

forall (X : eqType) (xs : seq X), 1 < size xs -> uniq xs -> exists a b : X, 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
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 *)
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
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
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
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
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
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
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. 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]]. *)

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]

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]
X: eqType
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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])
X: eqType
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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]
X: eqType
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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]
X: eqType
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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] = [::]
X: eqType
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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
a: X
xs: seq X
IHxs: forall (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]
P: X -> bool
f: X -> nat
t: nat
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. *)

forall (X : eqType) (R : rel X) (xs1 xs2 : seq X), transitive (T:=X) 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
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)
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
by rewrite //= path_sortedE //; apply/andP; split; last apply IHxs1 with (xs2 := 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
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
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. *)

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
X: eqType
a: X
xs: seq X
IHxs: forall d1 d2 : X, xs != [::] -> last d1 xs = last d2 xs

forall d1 d2 : X, a :: xs != [::] -> last d1 (a :: xs) = last d2 (a :: xs)
by intros * _; destruct xs. 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]. *)

forall (X : eqType) (xs : seq X) (d : X) (P : pred X), has P xs -> last d [seq x <- xs | P x] \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
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

forall (d : X) (P : pred X), has P (a :: 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
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
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
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
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
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

[::] = [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

[::] = [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
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
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
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]. *)

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
X: eqType
x: X
xs: seq X
IN: x \in rem_all x xs

False
X: eqType
x, a: X
xs: seq X
IN: x \in rem_all x (a :: xs)
IHxs: x \in rem_all x xs -> False

False
X: eqType
x, a: X
xs: seq X
IN: x \in rem_all x (a :: xs)

x \in rem_all x xs
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
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]. *)

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
X: eqType
a, x: X
xs: seq X
IN: a \in rem_all x xs

a \in xs
X: eqType
a, x, a0: X
xs: seq X
IN: a \in rem_all x (a0 :: xs)
IHxs: a \in rem_all x xs -> a \in xs

a \in a0 :: xs
X: eqType
a, x, a0: X
xs: seq X
IN: a \in (if a0 == x then rem_all x xs else a0 :: rem_all x xs)
IHxs: a \in rem_all x xs -> a \in xs

a \in a0 :: xs
X: eqType
a, x, a0: X
xs: seq X
EQ: (a0 == x) = true
IN: a \in rem_all x xs
IHxs: a \in rem_all x xs -> a \in xs

a \in a0 :: xs
X: eqType
a, x, a0: X
xs: seq X
EQ: (a0 == x) = false
IN: a \in a0 :: rem_all x xs
IHxs: a \in rem_all x xs -> a \in xs
a \in a0 :: xs
X: eqType
a, x, a0: X
xs: seq X
EQ: (a0 == x) = true
IN: a \in rem_all x xs
IHxs: a \in rem_all x xs -> a \in xs

a \in a0 :: xs
X: eqType
a, x, a0: X
xs: seq X
EQ: (a0 == x) = false
IN: a \in a0 :: rem_all x xs
IHxs: a \in rem_all x xs -> a \in xs
a \in a0 :: xs
X: eqType
a, x, a0: X
xs: seq X
EQ: (a0 == x) = false
IN: a \in a0 :: rem_all x xs
IHxs: a \in rem_all x xs -> a \in xs

a \in a0 :: xs
X: eqType
a, x, a0: X
xs: seq X
EQ: (a0 == x) = false
IN: a \in a0 :: rem_all x xs
IHxs: a \in rem_all x xs -> a \in xs

a \in a0 :: xs
X: eqType
a, x, a0: X
xs: seq X
EQ: (a0 == x) = false
IHxs: a \in rem_all x xs -> a \in xs
EQ2: a == a0

a \in a0 :: xs
X: eqType
a, x, a0: X
xs: seq X
EQ: (a0 == x) = false
IHxs: a \in rem_all x xs -> a \in xs
IN: a \in rem_all x xs
a \in a0 :: xs
X: eqType
a, x, a0: X
xs: seq X
EQ: (a0 == x) = false
IHxs: a \in rem_all x xs -> a \in xs
EQ2: a == a0

a \in a0 :: xs
X: eqType
a, x, a0: X
xs: seq X
EQ: (a0 == x) = false
IHxs: a \in rem_all x xs -> a \in xs
IN: a \in rem_all x xs
a \in a0 :: xs
X: eqType
a, x, a0: X
xs: seq X
EQ: (a0 == x) = false
IHxs: a \in rem_all x xs -> a \in xs
IN: a \in rem_all x xs

a \in a0 :: xs
X: eqType
a, x, a0: X
xs: seq X
EQ: (a0 == x) = false
IHxs: a \in rem_all x xs -> a \in xs
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]. *)

forall (x : nat) (xs : seq_predType nat_eqType), (forall y : nat, y \in xs -> x < y) -> rem_all x xs = xs

forall (x : nat) (xs : seq_predType nat_eqType), (forall y : nat, y \in xs -> x < y) -> rem_all x xs = xs
x: nat
a: nat_eqType
xs: seq nat_eqType
MIN: forall y : nat, y \in a :: xs -> x < y
IHxs: (forall y : nat, y \in xs -> x < y) -> rem_all x xs = xs

rem_all x (a :: xs) = a :: xs
x: nat
a: nat_eqType
xs: seq nat_eqType
MIN: forall y : nat, y \in a :: xs -> x < y
IHxs: (forall y : nat, y \in xs -> x < y) -> rem_all x xs = xs

(a == x) = false
x: nat
a: nat_eqType
xs: seq nat_eqType
MIN: forall y : nat, y \in a :: xs -> x < y
IHxs: (forall y : nat, y \in xs -> x < y) -> rem_all x xs = xs
a :: rem_all x xs = a :: xs
x: nat
a: nat_eqType
xs: seq nat_eqType
MIN: forall y : nat, y \in a :: xs -> x < y
IHxs: (forall y : nat, y \in xs -> x < y) -> rem_all x xs = xs

(a == x) = false
x: nat
a: nat_eqType
xs: seq nat_eqType
MIN: forall y : nat, y \in a :: xs -> x < y
IHxs: (forall y : nat, y \in xs -> x < y) -> rem_all x xs = xs

x < a
by apply MIN; rewrite in_cons; apply/orP; left.
x: nat
a: nat_eqType
xs: seq nat_eqType
MIN: forall y : nat, y \in a :: xs -> x < y
IHxs: (forall y : nat, y \in xs -> x < y) -> rem_all x xs = xs

a :: rem_all x xs = a :: xs
x: nat
a: nat_eqType
xs: seq nat_eqType
MIN: forall y : nat, y \in a :: xs -> x < y
IHxs: (forall y : nat, y \in xs -> x < y) -> rem_all x xs = xs

forall y : nat, y \in xs -> x < y
x: nat
a: nat_eqType
xs: seq nat_eqType
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]. *)

forall n_le m n : nat, 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)
n_le, m, n: nat
LE: n_le <= n

iota m n = iota m n_le ++ iota (m + n_le) (n - n_le)
n_le, m, k: nat

iota m (n_le + k) = iota m n_le ++ iota (m + n_le) (n_le + k - n_le)
n_le, m, k: nat

iota m n_le ++ iota (m + n_le) k = iota m n_le ++ iota (m + n_le) (n_le + k - n_le)
by replace (_ + _ - _) with k; last lia. Qed. (** Next, we prove that [index_iota a b = a :: index_iota a.+1 b] for [a < b]. *)

forall a b : nat, 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
a, b: nat
LT: a < b

iota a (b - a) = a :: iota a.+1 (b - a.+1)
a, b: nat
LT: a < b.+1

iota a (b.+1 - a) = a :: iota a.+1 (b.+1 - a.+1)
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. *)

forall (x : nat_eqType) (xs : seq nat_eqType) (k : nat), [seq ρ <- range 0 k | ρ \in [:: x, x & xs]] = [seq ρ <- range 0 k | ρ \in x :: xs]

forall (x : nat_eqType) (xs : seq nat_eqType) (k : nat), [seq ρ <- range 0 k | ρ \in [:: x, x & xs]] = [seq ρ <- range 0 k | ρ \in x :: xs]
x: nat_eqType
xs: seq nat_eqType
k: nat

[seq ρ <- range 0 k | ρ \in [:: x, x & xs]] = [seq ρ <- range 0 k | ρ \in x :: xs]
x: nat_eqType
xs: seq nat_eqType
k: nat
x0: nat_eqType

(x0 \in [:: x, x & xs]) = (x0 \in x :: xs)
x: nat_eqType
xs: seq nat_eqType
k: nat
x0: nat_eqType

[|| x0 == x, x0 == x | x0 \in xs] = (x0 == x) || (x0 \in xs)
by 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]. *)

forall x a b : nat, 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]
x, a, b: nat

a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
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]
x, a, b, k: nat
BO: b - a <= k

a <= 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]
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]
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]
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]
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]
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]
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]
b: nat
BO: b.+1 - 0 <= k.+1
LT: 0 < b.+1
GE: 0 <= 0

0 :: [seq ρ <- index_iota 1 b.+1 | ρ == 0] = [:: 0]
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]
b: nat
BO: b.+1 - 0 <= k.+1
LT: 0 < b.+1
GE: 0 <= 0

forall x : nat_eqType, x \in index_iota 1 b.+1 -> x != 0
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) = 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) = 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]
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]
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]
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]
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]
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]
a, b: nat
BO: b - a.+1 <= k.+1
LT: a.+1 < b
GE: a < a.+1

forall x : nat_eqType, x \in index_iota a.+2 b -> x != a.+1
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]
a, b: nat
BO: b - a.+1 <= k.+1
LT: a.+1 < b
GE: a < a.+1
x: nat_eqType
T1: a.+1 < x

x != a.+1
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) = 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) = 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]. *)

forall x a b : nat, 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]
x, a, b: nat
NEQ: a <= x < b

[seq ρ <- index_iota a b | ρ \in [:: x]] = [:: x]
x, a, b: nat
NEQ: a <= x < b

[seq ρ <- index_iota a b | ρ \in [:: x]] = [seq ρ <- index_iota a b | ρ == x]
x, a, b: nat
NEQ: a <= x < b
x0: nat_eqType

(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)]. *)

forall (a b x : nat) (xs : seq_predType nat_eqType), 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 nat_eqType), x < a -> [seq ρ <- index_iota a b | ρ \in xs] = [seq ρ <- index_iota a b | ρ \in rem_all x xs]
a, b, x: nat
xs: seq_predType nat_eqType
LT: x < a

[seq ρ <- index_iota a b | ρ \in xs] = [seq ρ <- index_iota a b | ρ \in rem_all x xs]
a, b, x: nat
xs: seq_predType nat_eqType
LT: x < a

{in index_iota a b, ssrfun.eqfun (fun ρ : nat => ρ \in xs) (fun ρ : nat_eqType => ρ \in rem_all x xs)}
a, b, x: nat
xs: seq_predType nat_eqType
LT: x < a
y: nat_eqType
LE: a <= y
GT: y < b

(y \in xs) = (y \in rem_all x xs)
a, b, x: nat
y': nat_eqType
xs: seq nat_eqType
LT: x < a
y: nat_eqType
LE: a <= y
GT: y < b
IHxs: (y \in xs) = (y \in rem_all x xs)

(y \in y' :: xs) = (y \in rem_all x (y' :: xs))
a, b, x: nat
y': nat_eqType
xs: seq nat_eqType
LT: x < a
y: nat_eqType
LE: a <= y
GT: y < b

(y == y') || (y \in rem_all x xs) = (y \in (if y' == x then rem_all x xs else y' :: rem_all x xs))
a, b, x: nat
y': nat_eqType
xs: seq nat_eqType
LT: x < a
y: nat_eqType
LE: a <= y
GT: y < b
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
y': nat_eqType
xs: seq nat_eqType
LT: x < a
y: nat_eqType
LE: a <= y
GT: y < b
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
y': nat_eqType
xs: seq nat_eqType
LT: x < a
y: nat_eqType
LE: a <= y
GT: y < b
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
y': nat_eqType
xs: seq nat_eqType
LT: x < a
y: nat_eqType
LE: a <= y
GT: y < b
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
y': nat_eqType
xs: seq nat_eqType
LT: x < a
y: nat_eqType
LE: a <= y
GT: y < b
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
y': nat_eqType
xs: seq nat_eqType
LT: x < a
y: nat_eqType
LE: a <= y
GT: y < b
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
y': nat_eqType
xs: seq nat_eqType
LT: x < a
y: nat_eqType
LE: a <= y
GT: y < b
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
y': nat_eqType
xs: seq nat_eqType
LT: x < a
y: nat_eqType
LE: a <= y
GT: y < b
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
y': nat_eqType
xs: seq nat_eqType
LT: x < a
y: nat_eqType
LE: a <= y
GT: y < b
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
y': nat_eqType
xs: seq nat_eqType
LT: x < a
y: nat_eqType
LE: a <= y
GT: y < b
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
y': nat_eqType
xs: seq nat_eqType
LT: x < a
y: nat_eqType
LE: a <= y
GT: y < b
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
y': nat_eqType
xs: seq nat_eqType
LT: x < a
y: nat_eqType
LE: a <= y
GT: y < b
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)]. *)

forall (x : nat) (xs : seq_predType nat_eqType) (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]

forall (x : nat) (xs : seq_predType nat_eqType) (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]
x: nat
xs: seq_predType nat_eqType
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]
x: nat
xs: seq_predType nat_eqType
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 nat_eqType
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 nat_eqType
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 nat_eqType
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 nat_eqType
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]
k: nat

forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType
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 nat_eqType) (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 nat_eqType
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]
k: nat
IHk: forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
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]
k: nat
IHk: forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
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]
k: nat
IHk: forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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]
k: nat
IHk: forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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]
k: nat
IHk: forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 ρ <- index_iota x.+1 b | ρ \in x :: xs]
k: nat
IHk: forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
b: nat
GT: x < b
MIN: forall y : nat, y \in xs -> x <= y
BO: b - x <= k.+1
true = (x \in x :: xs)
all: by auto; rewrite in_cons eq_refl.
k: nat
IHk: forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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])
k: nat
IHk: forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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])
k: nat
IHk: forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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)
k: nat
IHk: forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
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 :: [seq ρ <- index_iota x.+1 b | ρ \in rem_all x xs]
k: nat
IHk: forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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
k: nat
IHk: forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
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 :: [seq ρ <- index_iota x.+1 b | ρ \in rem_all x xs]
k: nat
IHk: forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 :: [seq ρ <- index_iota x.+1 b | ρ \in rem_all x xs]
k: nat
IHk: forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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]
k: nat
IHk: forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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)
k: nat
IHk: forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
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
k: nat
IHk: forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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)
k: nat
IHk: forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
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
k: nat
IHk: forall (x : nat) (xs : seq_predType nat_eqType) (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 nat_eqType
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 nat_eqType) (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 nat_eqType
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]. *)

forall (x : nat) (xs : seq_predType nat_eqType) (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]

forall (x : nat) (xs : seq_predType nat_eqType) (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]
x: nat
xs: seq_predType nat_eqType
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]. *)

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

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
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
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
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

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
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
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
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
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
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
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
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
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
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
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]
EQ: b - a = 0

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: 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: 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: a < b

x < nth 0 [seq x <- a :: 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
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
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.+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
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.+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]
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 = 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 = 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 = 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.