Library prosa.util.list


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)

Require Import prosa.util.ssrlia prosa.util.tactics.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

We define a few simple operations on lists. Namely first, last, and max.
Definition max0 := foldl maxn 0.
Definition first0 := head 0.
Definition last0 := last 0.

Additional lemmas about last0.
Section Last0.

Let [xs] be a non-empty sequence and [x] be an arbitrary element, then we prove that [last0 (x::xs) = last0 xs].
  Lemma last0_cons:
    ∀ x xs,
      xs ≠ [::] →
      last0 (x::xs) = last0 xs.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

  Proof.
    induction xs; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 43)
  
  x, a : nat
  xs : seq nat
  IHxs : xs <> [::] -> last0 (x :: xs) = last0 xs
  ============================
  a :: xs <> [::] -> last0 [:: x, a & xs] = last0 (a :: xs)

----------------------------------------------------------------------------- *)

    intros ?; by unfold last0.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Similarly, let [xs_r] be a non-empty sequence and [xs_l] be an sequence, we prove that [last0 (xs_l ++ xs_r) = last0 xs_r].
  Lemma last0_cat:
    ∀ xs_l xs_r,
      xs_r ≠ [::] →
      last0 (xs_l ++ xs_r) = last0 xs_r.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 45)
  
  ============================
  forall xs_l xs_r : seq nat,
  xs_r <> [::] -> last0 (xs_l ++ xs_r) = last0 xs_r

----------------------------------------------------------------------------- *)

  Proof.
    clear; induction xs_l; intros ? NEQ.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 56)
  
  xs_r : seq nat
  NEQ : xs_r <> [::]
  ============================
  last0 ([::] ++ xs_r) = last0 xs_r

subgoal 2 (ID 58) is:
 last0 ((a :: xs_l) ++ xs_r) = last0 xs_r

----------------------------------------------------------------------------- *)

    - by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 58)
  
  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

----------------------------------------------------------------------------- *)

    - simpl; rewrite last0_cons.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 66)
  
  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

subgoal 2 (ID 67) is:
 xs_l ++ xs_r <> [::]

----------------------------------------------------------------------------- *)

      apply IHxs_l; by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 67)
  
  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 <> [::]

----------------------------------------------------------------------------- *)

      intros C; apply: NEQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 76)
  
  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
  C : xs_l ++ xs_r = [::]
  ============================
  xs_r = [::]

----------------------------------------------------------------------------- *)

        by destruct xs_l.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

We also prove that [last0 xs = xs [| size xs -1 |] ].
  Lemma last0_nth:
    ∀ xs,
      last0 xs = nth 0 xs (size xs).-1.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

  Proof. by intros; rewrite nth_last.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

Qed.

We prove that for any non-empty sequence [xs] there is a sequence [xsh] such that [xsh ++ [::last0 x] = [xs]].
  Lemma last0_ex_cat:
    ∀ x xs,
      xs ≠ [::] →
      last0 xs = x →
      ∃ xsh, xsh ++ [::x] = xs.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

  Proof.
    clear; intros ? ? NEQ LAST.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 73)
  
  x : nat
  xs : seq nat
  NEQ : xs <> [::]
  LAST : last0 xs = x
  ============================
  exists xsh : seq nat, xsh ++ [:: x] = xs

----------------------------------------------------------------------------- *)

    induction xs; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 92)
  
  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

----------------------------------------------------------------------------- *)

    destruct xs.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 132)
  
  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]

subgoal 2 (ID 137) is:
 exists xsh : seq nat, xsh ++ [:: x] = [:: a, n & xs]

----------------------------------------------------------------------------- *)

    - ∃ [::]; by compute in LAST; subst a.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 137)
  
  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]

----------------------------------------------------------------------------- *)

    - feed_n 2 IHxs; try by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 159)
  
  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]

----------------------------------------------------------------------------- *)

      destruct IHxs as [xsh EQ].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 220)
  
  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 xsh0 : seq nat, xsh0 ++ [:: x] = [:: a, n & xs]

----------------------------------------------------------------------------- *)

      ∃ (a::xsh).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 223)
  
  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
  ============================
  (a :: xsh) ++ [:: x] = [:: a, n & xs]

----------------------------------------------------------------------------- *)

        by simpl; rewrite EQ.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

We prove that if [x] is the last element of a sequence [xs] and [x] satisfies a predicate, then [x] remains the last element in the filtered sequence.
  Lemma last0_filter:
    ∀ x xs (P : nat → bool),
      xs ≠ [::] →
      last0 xs = x →
      P x →
      last0 [seq x <- xs | P x] = x.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

  Proof.
    clear; intros ? ? ? NEQ LAST PX.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 89)
  
  x : nat
  xs : seq nat
  P : nat -> bool
  NEQ : xs <> [::]
  LAST : last0 xs = x
  PX : P x
  ============================
  last0 [seq x0 <- xs | P x0] = x

----------------------------------------------------------------------------- *)

    destruct (last0_ex_cat x xs NEQ LAST) as [xsh EQ]; subst xs.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 103)
  
  x : nat
  P : nat -> bool
  xsh : seq nat
  LAST : last0 (xsh ++ [:: x]) = x
  NEQ : xsh ++ [:: x] <> [::]
  PX : P x
  ============================
  last0 [seq x0 <- xsh ++ [:: x] | P x0] = x

----------------------------------------------------------------------------- *)

    rewrite filter_cat last0_cat.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 114)
  
  x : nat
  P : nat -> bool
  xsh : seq nat
  LAST : last0 (xsh ++ [:: x]) = x
  NEQ : xsh ++ [:: x] <> [::]
  PX : P x
  ============================
  last0 [seq x0 <- [:: x] | P x0] = x

subgoal 2 (ID 115) is:
 [seq x0 <- [:: x] | P x0] <> [::]

----------------------------------------------------------------------------- *)

    all:rewrite //= PX //=.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

End Last0.

Additional lemmas about max0.
Section Max0.

We prove that [max0 (x::xs)] is equal to [max {x, max0 xs}].
  Lemma max0_cons: ∀ x xs, max0 (x :: xs) = maxn x (max0 xs).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 28)
  
  ============================
  forall (x : nat) (xs : seq nat), max0 (x :: xs) = maxn x (max0 xs)

----------------------------------------------------------------------------- *)

  Proof.
    have L: ∀ s x xs, foldl maxn s (x::xs) = maxn x (foldl maxn s xs).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 40)
  
  ============================
  forall (s x : nat) (xs : seq nat),
  foldl maxn s (x :: xs) = maxn x (foldl maxn s xs)

subgoal 2 (ID 42) is:
 forall (x : nat) (xs : seq nat), max0 (x :: xs) = maxn x (max0 xs)

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 40)
  
  ============================
  forall (s x : nat) (xs : seq nat),
  foldl maxn s (x :: xs) = maxn x (foldl maxn s xs)

----------------------------------------------------------------------------- *)

clear; intros.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 45)
  
  s, x : nat
  xs : seq nat
  ============================
  foldl maxn s (x :: xs) = maxn x (foldl maxn s xs)

----------------------------------------------------------------------------- *)

      generalize dependent s; generalize dependent x.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 49)
  
  xs : seq nat
  ============================
  forall x s : nat, foldl maxn s (x :: xs) = maxn x (foldl maxn s xs)

----------------------------------------------------------------------------- *)

      induction xs.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 53)
  
  ============================
  forall x s : nat, foldl maxn s [:: x] = maxn x (foldl maxn s [::])

subgoal 2 (ID 57) is:
 forall x s : nat,
 foldl maxn s [:: x, a & xs] = maxn x (foldl maxn s (a :: xs))

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 53)
  
  ============================
  forall x s : nat, foldl maxn s [:: x] = maxn x (foldl maxn s [::])

----------------------------------------------------------------------------- *)

by intros; rewrite maxnC.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 57)

subgoal 1 (ID 57) is:
 forall x s : nat,
 foldl maxn s [:: x, a & xs] = maxn x (foldl maxn s (a :: xs))
subgoal 2 (ID 42) is:
 forall (x : nat) (xs : seq nat), max0 (x :: xs) = maxn x (max0 xs)

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

intros; simpl in ×.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 73)
  
  a : nat
  xs : seq nat
  IHxs : forall x s : nat,
         foldl maxn (maxn s x) xs = maxn x (foldl maxn s xs)
  x, s : nat
  ============================
  foldl maxn (maxn (maxn s x) a) xs = maxn x (foldl maxn (maxn s a) xs)

----------------------------------------------------------------------------- *)

          by rewrite maxnC IHxs [maxn s a]maxnC IHxs maxnA [maxn s x]maxnC.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 42)

subgoal 1 (ID 42) is:
 forall (x : nat) (xs : seq nat), max0 (x :: xs) = maxn x (max0 xs)

----------------------------------------------------------------------------- *)

      }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 42)

subgoal 1 (ID 42) is:
 forall (x : nat) (xs : seq nat), max0 (x :: xs) = maxn x (max0 xs)

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 42)
  
  L : forall (s x : nat) (xs : seq 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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Next, we prove that if all the numbers of a seq [xs] are equal to a constant [k], then [max0 xs = k].
  Lemma max0_of_uniform_set:
    ∀ k xs,
      size xs > 0 →
      (∀ x, x \in xs → x = k) →
      max0 xs = k.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

  Proof.
    clear; intros ? ? SIZE ALL.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

    induction xs; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 68)
  
  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

----------------------------------------------------------------------------- *)

    destruct xs.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 105)
  
  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

subgoal 2 (ID 110) is:
 max0 [:: a, s & xs] = k

----------------------------------------------------------------------------- *)

unfold max0; simpl; rewrite max0n; apply ALL.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 122)
  
  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]

subgoal 2 (ID 110) is:
 max0 [:: a, s & xs] = k

----------------------------------------------------------------------------- *)

by rewrite in_cons; apply/orP; left.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 110)
  
  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

----------------------------------------------------------------------------- *)

    rewrite max0_cons.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 158)
  
  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 (max0 (s :: xs)) = k

----------------------------------------------------------------------------- *)

    rewrite IHxs.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 162)
  
  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

subgoal 2 (ID 163) is:
 0 < size (s :: xs)
subgoal 3 (ID 164) is:
 forall x : nat_eqType, x \in s :: xs -> x = k

----------------------------------------------------------------------------- *)

    - by rewrite [a]ALL; [ rewrite maxnn | rewrite in_cons; apply/orP; left].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 163)
  
  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
  ============================
  0 < size (s :: xs)

subgoal 2 (ID 164) is:
 forall x : nat_eqType, x \in s :: xs -> x = k

----------------------------------------------------------------------------- *)

    - by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 164)
  
  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

----------------------------------------------------------------------------- *)

    - intros; apply ALL.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 209)
  
  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]

----------------------------------------------------------------------------- *)

      move: H; rewrite in_cons; move ⇒ /orP [/eqP EQ | IN].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 292)
  
  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]

subgoal 2 (ID 293) is:
 x \in [:: a, s & xs]

----------------------------------------------------------------------------- *)

      + by subst x; rewrite !in_cons; apply/orP; right; apply/orP; left.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 293)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

We prove that no element in a sequence [xs] is greater than [max0 xs].
  Lemma in_max0_le:
    ∀ xs x, x \in xs → x ≤ max0 xs.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

  Proof.
    induction xs; first by intros ?.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 66)
  
  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)

----------------------------------------------------------------------------- *)

    intros x; rewrite in_cons; move ⇒ /orP [/eqP EQ | IN]; subst.

(* ----------------------------------[ coqtop ]---------------------------------

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

subgoal 2 (ID 174) is:
 x <= max0 (a :: xs)

----------------------------------------------------------------------------- *)

    - by rewrite !max0_cons leq_maxl.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 174)
  
  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)

----------------------------------------------------------------------------- *)

    - apply leq_trans with (max0 xs); first eauto.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 188)
  
  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)

----------------------------------------------------------------------------- *)

      rewrite max0_cons.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 198)
  
  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 <= maxn a (max0 xs)

----------------------------------------------------------------------------- *)

        by apply leq_maxr.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

We prove that for a non-empty sequence [xs], [max0 xs ∈ xs].
  Lemma max0_in_seq:
    ∀ xs,
      xs ≠ [::] →
      max0 xs \in xs.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 68)
  
  ============================
  forall xs : seq nat, xs <> [::] -> max0 xs \in xs

----------------------------------------------------------------------------- *)

  Proof.
    clear; induction xs; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 77)
  
  a : nat
  xs : seq nat
  IHxs : xs <> [::] -> max0 xs \in xs
  ============================
  a :: xs <> [::] -> max0 (a :: xs) \in a :: xs

----------------------------------------------------------------------------- *)

    intros _; destruct xs.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 110)
  
  a : nat
  IHxs : [::] <> [::] -> max0 [::] \in [::]
  ============================
  max0 [:: a] \in [:: a]

subgoal 2 (ID 113) is:
 max0 [:: a, n & xs] \in [:: a, n & xs]

----------------------------------------------------------------------------- *)

    - destruct a; simpl.
(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 122)
  
  IHxs : [::] <> [::] -> max0 [::] \in [::]
  ============================
  max0 [:: 0] \in [:: 0]

subgoal 2 (ID 124) is:
 max0 [:: a.+1] \in [:: a.+1]
subgoal 3 (ID 113) is:
 max0 [:: a, n & xs] \in [:: a, n & xs]

----------------------------------------------------------------------------- *)

by done.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 124)
  
  a : nat
  IHxs : [::] <> [::] -> max0 [::] \in [::]
  ============================
  max0 [:: a.+1] \in [:: a.+1]

subgoal 2 (ID 113) is:
 max0 [:: a, n & xs] \in [:: a, n & xs]

----------------------------------------------------------------------------- *)

by rewrite /max0 //= max0n in_cons eq_refl.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 113)
  
  a, n : nat
  xs : seq nat
  IHxs : n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
  ============================
  max0 [:: a, n & xs] \in [:: a, n & xs]

----------------------------------------------------------------------------- *)

    - rewrite max0_cons.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 172)
  
  a, n : nat
  xs : seq nat
  IHxs : n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
  ============================
  maxn a (max0 (n :: xs)) \in [:: a, n & xs]

----------------------------------------------------------------------------- *)

      move: (leq_total a (max0 (n::xs))) ⇒ /orP [LE|LE].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 217)
  
  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]

subgoal 2 (ID 218) is:
 maxn a (max0 (n :: xs)) \in [:: a, n & xs]

----------------------------------------------------------------------------- *)

      + rewrite maxnE subnKC // in_cons; apply/orP; right.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 282)
  
  a, n : nat
  xs : seq nat
  IHxs : n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
  LE : a <= max0 (n :: xs)
  ============================
  max0 (n :: xs) \in n :: xs

subgoal 2 (ID 218) is:
 maxn a (max0 (n :: xs)) \in [:: a, n & xs]

----------------------------------------------------------------------------- *)

apply IHxs.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 283)
  
  a, n : nat
  xs : seq nat
  IHxs : n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
  LE : a <= max0 (n :: xs)
  ============================
  n :: xs <> [::]

subgoal 2 (ID 218) is:
 maxn a (max0 (n :: xs)) \in [:: a, n & xs]

----------------------------------------------------------------------------- *)

by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 218)
  
  a, n : nat
  xs : seq nat
  IHxs : n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
  LE : max0 (n :: xs) <= a
  ============================
  maxn a (max0 (n :: xs)) \in [:: a, n & xs]

----------------------------------------------------------------------------- *)

      + rewrite maxnE.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 315)
  
  a, n : nat
  xs : seq nat
  IHxs : n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
  LE : max0 (n :: xs) <= a
  ============================
  a + (max0 (n :: xs) - a) \in [:: a, n & xs]

----------------------------------------------------------------------------- *)

move: LE; rewrite -subn_eq0; move ⇒ /eqP EQ; rewrite EQ addn0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 362)
  
  a, n : nat
  xs : seq nat
  IHxs : n :: xs <> [::] -> max0 (n :: xs) \in n :: xs
  EQ : max0 (n :: xs) - a = 0
  ============================
  a \in [:: a, n & xs]

----------------------------------------------------------------------------- *)

          by rewrite in_cons; apply/orP; left.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Next we prove that one can remove duplicating element from the head of a sequence.
  Lemma max0_2cons_eq:
    ∀ x xs,
      max0 (x::x::xs) = max0 (x::xs).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 78)
  
  ============================
  forall (x : nat) (xs : seq nat), max0 [:: x, x & xs] = max0 (x :: xs)

----------------------------------------------------------------------------- *)

  Proof.
    intros; rewrite !max0_cons.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 88)
  
  x : nat
  xs : seq nat
  ============================
  maxn x (maxn x (max0 xs)) = maxn x (max0 xs)

----------------------------------------------------------------------------- *)

      by rewrite maxnA maxnn.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

We prove that one can remove the first element of a sequence if it is not greater than the second element of this sequence.
  Lemma max0_2cons_le:
    ∀ x1 x2 xs,
      x1 ≤ x2 →
      max0 (x1::x2::xs) = max0 (x2::xs).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 87)
  
  ============================
  forall (x1 x2 : nat) (xs : seq nat),
  x1 <= x2 -> max0 [:: x1, x2 & xs] = max0 (x2 :: xs)

----------------------------------------------------------------------------- *)

  Proof.
    intros; rewrite !max0_cons.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 99)
  
  x1, x2 : nat
  xs : seq nat
  H : x1 <= x2
  ============================
  maxn x1 (maxn x2 (max0 xs)) = maxn x2 (max0 xs)

----------------------------------------------------------------------------- *)

    rewrite maxnA.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 108)
  
  x1, x2 : nat
  xs : seq nat
  H : x1 <= x2
  ============================
  maxn (maxn x1 x2) (max0 xs) = maxn x2 (max0 xs)

----------------------------------------------------------------------------- *)

    rewrite [maxn x1 x2]maxnE subnKC //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

We prove that [max0] of a sequence [xs] is equal to [max0] of sequence [xs] without 0s.
  Lemma max0_rem0:
    ∀ xs,
      max0 ([seq x <- xs | 0 < x]) = max0 xs.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 93)
  
  ============================
  forall xs : seq nat, max0 [seq x <- xs | 0 < x] = max0 xs

----------------------------------------------------------------------------- *)

  Proof.
    induction xs; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 102)
  
  a : nat
  xs : seq nat
  IHxs : max0 [seq x <- xs | 0 < x] = max0 xs
  ============================
  max0 [seq x <- a :: xs | 0 < x] = max0 (a :: xs)

----------------------------------------------------------------------------- *)

    simpl; destruct a; simpl.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 119)
  
  xs : seq nat
  IHxs : max0 [seq x <- xs | 0 < x] = max0 xs
  ============================
  max0 [seq x <- xs | 0 < x] = max0 (0 :: xs)

subgoal 2 (ID 124) is:
 max0 (a.+1 :: [seq x <- xs | 0 < x]) = max0 (a.+1 :: xs)

----------------------------------------------------------------------------- *)

    - by rewrite max0_cons max0n.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 124)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Note that the last element is at most the max element.
  Lemma last_of_seq_le_max_of_seq:
    ∀ xs, last0 xs ≤ max0 xs.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 95)
  
  ============================
  forall xs : seq nat, last0 xs <= max0 xs

----------------------------------------------------------------------------- *)

  Proof.
    intros xs.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 96)
  
  xs : seq nat
  ============================
  last0 xs <= max0 xs

----------------------------------------------------------------------------- *)

    have EX: ∃ len, size xs ≤ len.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 100)
  
  xs : seq nat
  ============================
  exists len : nat, size xs <= len

subgoal 2 (ID 102) is:
 last0 xs <= max0 xs

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 100)
  
  xs : seq nat
  ============================
  exists len : nat, size xs <= len

----------------------------------------------------------------------------- *)

∃ (size xs).
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 105)
  
  xs : seq nat
  ============================
  size xs <= size xs

----------------------------------------------------------------------------- *)

by done.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 102)

subgoal 1 (ID 102) is:
 last0 xs <= max0 xs

----------------------------------------------------------------------------- *)

}
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 102)
  
  xs : seq nat
  EX : exists len : nat, size xs <= len
  ============================
  last0 xs <= max0 xs

----------------------------------------------------------------------------- *)


    move: EX ⇒ [len LE].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 118)
  
  xs : seq nat
  len : nat
  LE : size xs <= len
  ============================
  last0 xs <= max0 xs

----------------------------------------------------------------------------- *)

    generalize dependent xs.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 120)
  
  len : nat
  ============================
  forall xs : seq nat, size xs <= len -> last0 xs <= max0 xs

----------------------------------------------------------------------------- *)

    induction len.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 124)
  
  ============================
  forall xs : seq nat, size xs <= 0 -> last0 xs <= max0 xs

subgoal 2 (ID 127) is:
 forall xs : seq nat, size xs <= len.+1 -> last0 xs <= max0 xs

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 124)
  
  ============================
  forall xs : seq nat, size xs <= 0 -> last0 xs <= max0 xs

----------------------------------------------------------------------------- *)

by intros; move: LE; rewrite leqn0 size_eq0; move ⇒ /eqP EQ; subst.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 127)

subgoal 1 (ID 127) is:
 forall xs : seq nat, size xs <= len.+1 -> last0 xs <= max0 xs

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 127)
  
  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

----------------------------------------------------------------------------- *)

    intros ? SIZE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 176)
  
  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

----------------------------------------------------------------------------- *)

    move: SIZE; rewrite leq_eqVlt; move ⇒ /orP [/eqP EQ| LE]; last first.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 258)
  
  len : nat
  IHlen : forall xs : seq nat, size xs <= len -> last0 xs <= max0 xs
  xs : seq nat
  LE : size xs < len.+1
  ============================
  last0 xs <= max0 xs

subgoal 2 (ID 257) is:
 last0 xs <= max0 xs

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 258)
  
  len : nat
  IHlen : forall xs : seq nat, size xs <= len -> last0 xs <= max0 xs
  xs : seq nat
  LE : size xs < len.+1
  ============================
  last0 xs <= max0 xs

----------------------------------------------------------------------------- *)

by apply IHlen.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 257)

subgoal 1 (ID 257) is:
 last0 xs <= max0 xs

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 257)
  
  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

----------------------------------------------------------------------------- *)

    destruct xs as [ | x1 xs]; first by inversion EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 271)
  
  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)

----------------------------------------------------------------------------- *)

    destruct xs as [ | x2 xs].
(* ----------------------------------[ coqtop ]---------------------------------

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

subgoal 2 (ID 292) is:
 last0 [:: x1, x2 & xs] <= max0 [:: x1, x2 & xs]

----------------------------------------------------------------------------- *)

by rewrite /max leq_max; apply/orP; right.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 292)
  
  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]

----------------------------------------------------------------------------- *)

    have F1: last0 [:: x1, x2 & xs] = last0 [:: x2 & xs] by done.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 332)
  
  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
  F1 : last0 [:: x1, x2 & xs] = last0 (x2 :: xs)
  ============================
  last0 [:: x1, x2 & xs] <= max0 [:: x1, x2 & xs]

----------------------------------------------------------------------------- *)

    rewrite F1 max0_cons; clear F1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 339)
  
  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) <= maxn x1 (max0 (x2 :: xs))

----------------------------------------------------------------------------- *)

    rewrite leq_max; apply/orP; right.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 370)
  
  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 (x2 :: xs)

----------------------------------------------------------------------------- *)

    apply IHlen.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 371)
  
  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

----------------------------------------------------------------------------- *)

    move: EQ ⇒ /eqP; simpl; rewrite eqSS; move ⇒ /eqP EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 474)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  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 max of [xs] is less-than-or-equal-to max of [ys].
  Lemma max_of_dominating_seq:
    ∀ (xs ys : seq nat),
      (∀ n, xs[|n|] ≤ ys[|n|]) →
      max0 xs ≤ max0 ys.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

  Proof.
    intros xs ys.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

    have EX: ∃ len, size xs ≤ len ∧ size ys ≤ len.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 106)
  
  xs, ys : seq nat
  ============================
  exists len : nat, size xs <= len /\ size ys <= len

subgoal 2 (ID 108) is:
 (forall n : nat, xs [|n|] <= ys [|n|]) -> max0 xs <= max0 ys

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 106)
  
  xs, ys : seq nat
  ============================
  exists len : nat, size xs <= len /\ size ys <= len

----------------------------------------------------------------------------- *)

∃ (maxn (size xs) (size ys)).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 112)
  
  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].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 108)

subgoal 1 (ID 108) is:
 (forall n : nat, xs [|n|] <= ys [|n|]) -> max0 xs <= max0 ys

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 108)
  
  xs, ys : seq nat
  EX : exists len : nat, size xs <= len /\ size ys <= len
  ============================
  (forall n : nat, xs [|n|] <= ys [|n|]) -> max0 xs <= max0 ys

----------------------------------------------------------------------------- *)

    move: EX ⇒ [len [LE1 LE2]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 200)
  
  xs, ys : seq nat
  len : nat
  LE1 : size xs <= len
  LE2 : size ys <= len
  ============================
  (forall n : nat, xs [|n|] <= ys [|n|]) -> max0 xs <= max0 ys

----------------------------------------------------------------------------- *)

    generalize dependent xs; generalize dependent ys.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 204)
  
  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

----------------------------------------------------------------------------- *)

    induction len; intros.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 216)
  
  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

subgoal 2 (ID 221) is:
 max0 xs <= max0 ys

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 216)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 221)

subgoal 1 (ID 221) is:
 max0 xs <= max0 ys

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 221)
  
  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

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 221)
  
  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

----------------------------------------------------------------------------- *)

destruct xs, ys; try done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 370)
  
  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 [::]

subgoal 2 (ID 377) is:
 max0 (n :: xs) <= max0 (n0 :: ys)

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 370)
  
  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 [::]

----------------------------------------------------------------------------- *)

have L: ∀ xs, (∀ n, xs [| n |] = 0) → max0 xs = 0.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 429)
  
  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 xs0 : seq nat, (forall n0 : nat, xs0 [|n0|] = 0) -> max0 xs0 = 0

subgoal 2 (ID 431) is:
 max0 (n :: xs) <= max0 [::]

----------------------------------------------------------------------------- *)

        {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 429)
  
  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 xs0 : seq nat, (forall n0 : nat, xs0 [|n0|] = 0) -> max0 xs0 = 0

----------------------------------------------------------------------------- *)

clear; intros.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 434)
  
  xs : seq nat
  H : forall n : nat, xs [|n|] = 0
  ============================
  max0 xs = 0

----------------------------------------------------------------------------- *)

          induction xs; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 448)
  
  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

----------------------------------------------------------------------------- *)

          rewrite max0_cons.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 452)
  
  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

----------------------------------------------------------------------------- *)

          apply/eqP; rewrite eqn_leq; apply/andP; split; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 537)
  
  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

----------------------------------------------------------------------------- *)

          rewrite geq_max; apply/andP; split.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 569)
  
  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

subgoal 2 (ID 570) is:
 max0 xs <= 0

----------------------------------------------------------------------------- *)

          - by specialize (H 0); simpl in H; rewrite H.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 570)
  
  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

----------------------------------------------------------------------------- *)

          - rewrite leqn0; apply/eqP; apply: IHxs.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 613)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 431)

subgoal 1 (ID 431) is:
 max0 (n :: xs) <= max0 [::]
subgoal 2 (ID 377) is:
 max0 (n :: xs) <= max0 (n0 :: ys)

----------------------------------------------------------------------------- *)

        }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 431)
  
  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 [::]

----------------------------------------------------------------------------- *)

        rewrite L; first by done.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 623)
  
  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

----------------------------------------------------------------------------- *)

        intros; specialize (H n0).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 626)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 377)

subgoal 1 (ID 377) is:
 max0 (n :: xs) <= max0 (n0 :: ys)

----------------------------------------------------------------------------- *)

      }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 377)
  
  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)

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 377)
  
  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)

----------------------------------------------------------------------------- *)

rewrite !max0_cons.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 778)
  
  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|]
  ============================
  maxn n (max0 xs) <= maxn n0 (max0 ys)

----------------------------------------------------------------------------- *)

        rewrite geq_max; apply/andP; split.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 811)
  
  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)

subgoal 2 (ID 812) is:
 max0 xs <= maxn n0 (max0 ys)

----------------------------------------------------------------------------- *)

        + rewrite leq_max; apply/orP; left.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 843)
  
  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

subgoal 2 (ID 812) is:
 max0 xs <= maxn n0 (max0 ys)

----------------------------------------------------------------------------- *)

            by specialize (H 0); simpl in H.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 812)
  
  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)

----------------------------------------------------------------------------- *)

        + rewrite leq_max; apply/orP; right.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 879)
  
  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

----------------------------------------------------------------------------- *)

          apply IHlen; try (by rewrite ltnS in LE1, LE2).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 882)
  
  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 n1 : nat, xs [|n1|] <= ys [|n1|]

----------------------------------------------------------------------------- *)

            by intros; specialize (H n1.+1); simpl in H.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

      }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

End Max0.

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

  (* We prove that if [x] lies in [xs] excluding [y], then [x] also lies in [xs]. *)
  Lemma rem_in:
    ∀ (T: eqType) (x y: T) (xs: seq T),
      x \in rem y xs → x \in xs.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 31)
  
  ============================
  forall (T : eqType) (x y : T) (xs : seq T),
  x \in rem (T:=T) y xs -> x \in xs

----------------------------------------------------------------------------- *)

  Proof.
    clear; intros.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 36)
  
  T : eqType
  x, y : T
  xs : seq T
  H : x \in rem (T:=T) y xs
  ============================
  x \in xs

----------------------------------------------------------------------------- *)

    induction xs; simpl in H.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 52)
  
  T : eqType
  x, y : T
  H : x \in [::]
  ============================
  x \in [::]

subgoal 2 (ID 54) is:
 x \in a :: xs

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 52)
  
  T : eqType
  x, y : T
  H : x \in [::]
  ============================
  x \in [::]

----------------------------------------------------------------------------- *)

by rewrite in_nil in H.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 54)

subgoal 1 (ID 54) is:
 x \in a :: xs

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

rewrite in_cons; apply/orP.

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 99)
  
  T : eqType
  x, y, a : T
  xs : seq T
  H : x \in (if a == y then xs else a :: rem (T:=T) y xs)
  IHxs : x \in rem (T:=T) y xs -> x \in xs
  ============================
  x == a \/ x \in xs

----------------------------------------------------------------------------- *)

      destruct (a == y) eqn:EQ.
(* ----------------------------------[ coqtop ]---------------------------------

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

subgoal 2 (ID 123) is:
 x == a \/ x \in xs

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

by move: EQ ⇒ /eqP EQ; subst a; right.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 123)

subgoal 1 (ID 123) is:
 x == a \/ x \in xs

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

move: H; rewrite in_cons; move ⇒ /orP [/eqP H | H].

(* ----------------------------------[ coqtop ]---------------------------------

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

subgoal 2 (ID 247) is:
 x == a \/ x \in xs

----------------------------------------------------------------------------- *)

        - by subst a; left.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

        - by right; apply IHxs.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

      }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

  (* We prove that if we remove an element [x] for which [P x] from 
     a filter, then the size of the filter decreases by [1]. *)
  Lemma filter_size_rem:
    ∀ (T: eqType) (x:T) (xs: seq T) (P: T → bool),
      (x \in xs) →
      P x →
      size [seq y <- xs | P y] = size [seq y <- rem x xs | P y] + 1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 45)
  
  ============================
  forall (T : eqType) (x : T) (xs : seq T) (P : T -> bool),
  x \in xs ->
  P x -> size [seq y <- xs | P y] = size [seq y <- rem (T:=T) x xs | P y] + 1

----------------------------------------------------------------------------- *)

  Proof.
    clear; intros.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 51)
  
  T : eqType
  x : T
  xs : seq T
  P : T -> bool
  H : x \in xs
  H0 : P x
  ============================
  size [seq y <- xs | P y] = size [seq y <- rem (T:=T) x xs | P y] + 1

----------------------------------------------------------------------------- *)

    induction xs; first by inversion H.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 68)
  
  T : eqType
  x, a : T
  xs : seq T
  P : T -> bool
  H : x \in a :: xs
  H0 : P x
  IHxs : x \in xs ->
         size [seq y <- xs | P y] = size [seq y <- rem (T:=T) x xs | P y] + 1
  ============================
  size [seq y <- a :: xs | P y] =
  size [seq y <- rem (T:=T) x (a :: xs) | P y] + 1

----------------------------------------------------------------------------- *)

    move: H; rewrite in_cons; move ⇒ /orP [/eqP H | H]; subst.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 169)
  
  T : eqType
  a : T
  xs : seq T
  P : T -> bool
  IHxs : a \in xs ->
         size [seq y <- xs | P y] = size [seq y <- rem (T:=T) a xs | P y] + 1
  H0 : P a
  ============================
  size [seq y <- a :: xs | P y] =
  size [seq y <- rem (T:=T) a (a :: xs) | P y] + 1

subgoal 2 (ID 161) is:
 size [seq y <- a :: xs | P y] =
 size [seq y <- rem (T:=T) x (a :: xs) | P y] + 1

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 169)
  
  T : eqType
  a : T
  xs : seq T
  P : T -> bool
  IHxs : a \in xs ->
         size [seq y <- xs | P y] = size [seq y <- rem (T:=T) a xs | P y] + 1
  H0 : P a
  ============================
  size [seq y <- a :: xs | P y] =
  size [seq y <- rem (T:=T) a (a :: xs) | P y] + 1

----------------------------------------------------------------------------- *)

by simpl; rewrite H0 -[X in X = _]addn1 eq_refl.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 161)

subgoal 1 (ID 161) is:
 size [seq y <- a :: xs | P y] =
 size [seq y <- rem (T:=T) x (a :: xs) | P y] + 1

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 161)
  
  T : eqType
  x, a : T
  xs : seq T
  P : T -> bool
  H0 : P x
  IHxs : x \in xs ->
         size [seq y <- xs | P y] = size [seq y <- rem (T:=T) x xs | P y] + 1
  H : x \in xs
  ============================
  size [seq y <- a :: xs | P y] =
  size [seq y <- rem (T:=T) x (a :: xs) | P y] + 1

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 161)
  
  T : eqType
  x, a : T
  xs : seq T
  P : T -> bool
  H0 : P x
  IHxs : x \in xs ->
         size [seq y <- xs | P y] = size [seq y <- rem (T:=T) x xs | P y] + 1
  H : x \in xs
  ============================
  size [seq y <- a :: xs | P y] =
  size [seq y <- rem (T:=T) x (a :: xs) | P y] + 1

----------------------------------------------------------------------------- *)

specialize (IHxs H); simpl in ×.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 207)
  
  T : eqType
  x, a : T
  xs : seq T
  P : T -> bool
  H0 : P x
  IHxs : size [seq y <- xs | P y] = size [seq y <- rem (T:=T) 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:=T) x xs | P y] + 1

----------------------------------------------------------------------------- *)

      case EQab: (a == x); simpl.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 238)
  
  T : eqType
  x, a : T
  xs : seq T
  P : T -> bool
  H0 : P x
  IHxs : size [seq y <- xs | P y] = size [seq y <- rem (T:=T) 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

subgoal 2 (ID 244) is:
 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:=T) x xs | P y]
    else [seq y <- rem (T:=T) x xs | P y]) + 1

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 238)
  
  T : eqType
  x, a : T
  xs : seq T
  P : T -> bool
  H0 : P x
  IHxs : size [seq y <- xs | P y] = size [seq y <- rem (T:=T) x xs | P y] + 1
  H : x \in xs
  EQab : (a == x) = true
  ============================
  size (if P a then a :: [seq y <- xs | P y] else [seq y <- xs | P y]) =
  size [seq y <- xs | P y] + 1

----------------------------------------------------------------------------- *)

move: EQab ⇒ /eqP EQab; subst.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 282)
  
  T : eqType
  x : T
  xs : seq T
  P : T -> bool
  H0 : P x
  IHxs : size [seq y <- xs | P y] = size [seq y <- rem (T:=T) 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.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 244)

subgoal 1 (ID 244) is:
 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:=T) x xs | P y]
    else [seq y <- rem (T:=T) x xs | P y]) + 1

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 244)
  
  T : eqType
  x, a : T
  xs : seq T
  P : T -> bool
  H0 : P x
  IHxs : size [seq y <- xs | P y] = size [seq y <- rem (T:=T) 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:=T) x xs | P y]
     else [seq y <- rem (T:=T) x xs | P y]) + 1

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 244)
  
  T : eqType
  x, a : T
  xs : seq T
  P : T -> bool
  H0 : P x
  IHxs : size [seq y <- xs | P y] = size [seq y <- rem (T:=T) 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:=T) x xs | P y]
     else [seq y <- rem (T:=T) x xs | P y]) + 1

----------------------------------------------------------------------------- *)

case Pa: (P a); simpl.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 321)
  
  T : eqType
  x, a : T
  xs : seq T
  P : T -> bool
  H0 : P x
  IHxs : size [seq y <- xs | P y] = size [seq y <- rem (T:=T) 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:=T) x xs | P y]).+1 + 1

subgoal 2 (ID 323) is:
 size [seq y <- xs | P y] = size [seq y <- rem (T:=T) x xs | P y] + 1

----------------------------------------------------------------------------- *)

        - by rewrite IHxs !addn1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 323)
  
  T : eqType
  x, a : T
  xs : seq T
  P : T -> bool
  H0 : P x
  IHxs : size [seq y <- xs | P y] = size [seq y <- rem (T:=T) 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:=T) x xs | P y] + 1

----------------------------------------------------------------------------- *)

        - by rewrite IHxs.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

      }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

End RemList.

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

  (* First, we show that if [n > 0], then [nth (x::xs) n = nth xs (n-1)]. *)
  Lemma nth0_cons:
    ∀ x xs n,
      n > 0 →
      nth 0 (x :: xs) n = nth 0 xs n.-1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 31)
  
  ============================
  forall (x : nat) (xs : seq nat) (n : nat),
  0 < n -> nth 0 (x :: xs) n = nth 0 xs n.-1

----------------------------------------------------------------------------- *)

  Proof. by intros; destruct n.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

Qed.

  (* We prove that a sequence [xs] of size [n.+1] can be destructed
     into a sequence [xs_l] of size [n] and an element [x] such that
     [x = xs ++ [::x]]. *)
  Lemma seq_elim_last:
    ∀ {X : Type} (n : nat) (xs : seq X),
      size xs = n.+1 →
      ∃ x xs__c, xs = xs__c ++ [:: x] ∧ size xs__c = n.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 50)
  
  ============================
  forall (X : Type) (n : nat) (xs : seq X),
  size xs = n.+1 ->
  exists (x : X) (xs__c : seq X), xs = xs__c ++ [:: x] /\ size xs__c = n

----------------------------------------------------------------------------- *)

  Proof.
    intros ? ? ? SIZE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 54)
  
  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

----------------------------------------------------------------------------- *)

    revert xs SIZE; induction n; intros.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 65)
  
  X : Type
  xs : seq X
  SIZE : size xs = 1
  ============================
  exists (x : X) (xs__c : seq X), xs = xs__c ++ [:: x] /\ size xs__c = 0

subgoal 2 (ID 67) is:
 exists (x : X) (xs__c : seq X), xs = xs__c ++ [:: x] /\ size xs__c = n.+1

----------------------------------------------------------------------------- *)

    - destruct xs; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 79)
  
  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

subgoal 2 (ID 67) is:
 exists (x : X) (xs__c : seq X), xs = xs__c ++ [:: x] /\ size xs__c = n.+1

----------------------------------------------------------------------------- *)

      destruct xs; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 115)
  
  X : Type
  x : X
  SIZE : size [:: x] = 1
  ============================
  exists (x0 : X) (xs__c : seq X),
    [:: x] = xs__c ++ [:: x0] /\ size xs__c = 0

subgoal 2 (ID 67) is:
 exists (x : X) (xs__c : seq X), xs = xs__c ++ [:: x] /\ size xs__c = n.+1

----------------------------------------------------------------------------- *)

      ∃ x, [::]; split; by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 67)
  
  X : Type
  n : nat
  IHn : forall xs : seq X,
        size xs = n.+1 ->
        exists (x : X) (xs__c : seq X),
          xs = xs__c ++ [:: x] /\ size xs__c = n
  xs : seq X
  SIZE : size xs = n.+2
  ============================
  exists (x : X) (xs__c : seq X), xs = xs__c ++ [:: x] /\ size xs__c = n.+1

----------------------------------------------------------------------------- *)

    - destruct xs; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 165)
  
  X : Type
  n : nat
  IHn : forall xs : seq X,
        size xs = n.+1 ->
        exists (x : X) (xs__c : seq X),
          xs = xs__c ++ [:: x] /\ size xs__c = n
  x : X
  xs : seq X
  SIZE : size (x :: xs) = n.+2
  ============================
  exists (x0 : X) (xs__c : seq X),
    x :: xs = xs__c ++ [:: x0] /\ size xs__c = n.+1

----------------------------------------------------------------------------- *)

      specialize (IHn xs).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 194)
  
  X : Type
  n : nat
  xs : seq X
  IHn : size xs = n.+1 ->
        exists (x : X) (xs__c : seq X),
          xs = xs__c ++ [:: x] /\ size xs__c = n
  x : X
  SIZE : size (x :: xs) = n.+2
  ============================
  exists (x0 : X) (xs__c : seq X),
    x :: xs = xs__c ++ [:: x0] /\ size xs__c = n.+1

----------------------------------------------------------------------------- *)

      feed IHn; first by simpl in SIZE; apply eq_add_S in SIZE.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 200)
  
  X : Type
  n : nat
  xs : seq X
  IHn : exists (x : X) (xs__c : seq X),
          xs = xs__c ++ [:: x] /\ size xs__c = n
  x : X
  SIZE : size (x :: xs) = n.+2
  ============================
  exists (x0 : X) (xs__c : seq X),
    x :: xs = xs__c ++ [:: x0] /\ size xs__c = n.+1

----------------------------------------------------------------------------- *)

      destruct IHn as [x__n [xs__n [EQ__n SIZE__n]]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 223)
  
  X : Type
  n : nat
  xs : seq X
  x__n : X
  xs__n : seq X
  EQ__n : xs = xs__n ++ [:: x__n]
  SIZE__n : size xs__n = 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

----------------------------------------------------------------------------- *)

      subst xs.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 229)
  
  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__n, (x :: xs__n); split; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 237)
  
  X : Type
  n : nat
  x__n : X
  xs__n : seq X
  SIZE__n : size xs__n = n
  x : X
  SIZE : size (x :: xs__n ++ [:: x__n]) = n.+2
  ============================
  size (x :: xs__n) = n.+1

----------------------------------------------------------------------------- *)

      simpl in SIZE; apply eq_add_S in SIZE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 240)
  
  X : Type
  n : nat
  x__n : X
  xs__n : seq X
  SIZE__n : size xs__n = n
  x : X
  SIZE : size (xs__n ++ [:: x__n]) = n.+1
  ============================
  size (x :: xs__n) = n.+1

----------------------------------------------------------------------------- *)

      rewrite size_cat in SIZE; simpl in SIZE; rewrite addn1 in SIZE; apply eq_add_S in SIZE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 281)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

  (* Next, we prove that [x ∈ xs] implies that [xs] can be split 
     into two parts such that [xs = xsl ++ [::x] ++ [xsr]]. *)
  Lemma in_cat:
    ∀ {X : eqType} (x : X) (xs : list X),
      x \in xs → ∃ xsl xsr, xs = xsl ++ [::x] ++ xsr.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

  Proof.
    intros ? ? ? SUB.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 70)
  
  X : eqType
  x : X
  xs : seq X
  SUB : x \in xs
  ============================
  exists xsl xsr : seq X, xs = xsl ++ [:: x] ++ xsr

----------------------------------------------------------------------------- *)

    induction xs; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 84)
  
  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

----------------------------------------------------------------------------- *)

    move: SUB; rewrite in_cons; move ⇒ /orP [/eqP EQ|IN].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 194)
  
  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

subgoal 2 (ID 195) is:
 exists xsl xsr : seq X, a :: xs = xsl ++ [:: x] ++ xsr

----------------------------------------------------------------------------- *)

    - by subst; ∃ [::], xs.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 195)
  
  X : eqType
  x, a : X
  xs : seq X
  IHxs : x \in xs -> exists xsl xsr : seq X, xs = xsl ++ [:: x] ++ xsr
  IN : x \in xs
  ============================
  exists xsl xsr : seq X, a :: xs = xsl ++ [:: x] ++ xsr

----------------------------------------------------------------------------- *)

    - feed IHxs; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 212)
  
  X : eqType
  x, a : X
  xs : seq X
  IHxs : exists xsl xsr : seq X, xs = xsl ++ [:: x] ++ xsr
  IN : x \in xs
  ============================
  exists xsl xsr : seq X, a :: xs = xsl ++ [:: x] ++ xsr

----------------------------------------------------------------------------- *)

      clear IN; move: IHxs ⇒ [xsl [xsr EQ]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 236)
  
  X : eqType
  x, a : X
  xs, xsl, xsr : seq X
  EQ : xs = xsl ++ [:: x] ++ xsr
  ============================
  exists xsl0 xsr0 : seq X, a :: xs = xsl0 ++ [:: x] ++ xsr0

----------------------------------------------------------------------------- *)

        by subst; ∃ (a::xsl), xsr.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

  (* We prove that for any two sequences [xs] and [ys] the fact that [xs] is a sub-sequence 
     of [ys] implies that the size of [xs] is at most the size of [ys]. *)
  Lemma subseq_leq_size:
    ∀ {X : eqType} (xs ys: seq X),
      uniq xs →
      (∀ x, x \in xs → x \in ys) →
      size xs ≤ size ys.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 80)
  
  ============================
  forall (X : eqType) (xs ys : seq X),
  uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys

----------------------------------------------------------------------------- *)

  Proof.
    clear; intros ? ? ? UNIQ SUB.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 85)
  
  X : eqType
  xs, ys : seq X
  UNIQ : uniq xs
  SUB : forall x : X, x \in xs -> x \in ys
  ============================
  size xs <= size ys

----------------------------------------------------------------------------- *)

    have EXm: ∃ m, size ys ≤ m; first by ∃ (size ys).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 91)
  
  X : eqType
  xs, ys : seq X
  UNIQ : uniq xs
  SUB : forall x : X, x \in xs -> x \in ys
  EXm : exists m : nat, size ys <= m
  ============================
  size xs <= size ys

----------------------------------------------------------------------------- *)

    move: EXm ⇒ [m SIZEm].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 107)
  
  X : eqType
  xs, ys : seq X
  UNIQ : uniq xs
  SUB : forall x : X, x \in xs -> x \in ys
  m : nat
  SIZEm : size ys <= m
  ============================
  size xs <= size ys

----------------------------------------------------------------------------- *)

    move: SIZEm UNIQ SUB; move: xs ys.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 117)
  
  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

----------------------------------------------------------------------------- *)

    induction m; intros.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 129)
  
  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

subgoal 2 (ID 134) is:
 size xs <= size ys

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 129)
  
  X : eqType
  xs, ys : seq X
  SIZEm : size ys <= 0
  UNIQ : uniq xs
  SUB : forall x : X, x \in xs -> x \in ys
  ============================
  size xs <= size ys

----------------------------------------------------------------------------- *)

move: SIZEm; rewrite leqn0 size_eq0; move ⇒ /eqP SIZEm; subst ys.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 183)
  
  X : eqType
  xs : seq X
  UNIQ : uniq xs
  SUB : forall x : X, x \in xs -> x \in [::]
  ============================
  size xs <= size [::]

----------------------------------------------------------------------------- *)

      destruct xs; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 199)
  
  X : eqType
  s : X
  xs : seq X
  UNIQ : uniq (s :: xs)
  SUB : forall x : X, x \in s :: xs -> x \in [::]
  ============================
  size (s :: xs) <= size [::]

----------------------------------------------------------------------------- *)

      specialize (SUB s).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 201)
  
  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].
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 134)

subgoal 1 (ID 134) is:
 size xs <= size ys

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 134)
  
  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

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 134)
  
  X : eqType
  m : nat
  IHm : forall xs ys : seq X,
        size ys <= m ->
        uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
  xs, ys : seq X
  SIZEm : size ys <= m.+1
  UNIQ : uniq xs
  SUB : forall x : X, x \in xs -> x \in ys
  ============================
  size xs <= size ys

----------------------------------------------------------------------------- *)

destruct xs as [ | x xs]; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 257)
  
  X : eqType
  m : nat
  IHm : forall xs ys : seq X,
        size ys <= m ->
        uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
  x : X
  xs, ys : seq X
  SIZEm : size ys <= m.+1
  UNIQ : uniq (x :: xs)
  SUB : forall x0 : X, x0 \in x :: xs -> x0 \in ys
  ============================
  size (x :: xs) <= size ys

----------------------------------------------------------------------------- *)

      move: (@in_cat _ x ys) ⇒ Lem.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 261)
  
  X : eqType
  m : nat
  IHm : forall xs ys : seq X,
        size ys <= m ->
        uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
  x : X
  xs, ys : seq X
  SIZEm : size ys <= m.+1
  UNIQ : uniq (x :: xs)
  SUB : forall x0 : X, x0 \in x :: xs -> x0 \in ys
  Lem : x \in ys -> exists xsl xsr : seq X, ys = xsl ++ [:: x] ++ xsr
  ============================
  size (x :: xs) <= size ys

----------------------------------------------------------------------------- *)

      feed Lem; first by apply SUB; rewrite in_cons; apply/orP; left.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 267)
  
  X : eqType
  m : nat
  IHm : forall xs ys : seq X,
        size ys <= m ->
        uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
  x : X
  xs, ys : seq X
  SIZEm : size ys <= m.+1
  UNIQ : uniq (x :: xs)
  SUB : forall x0 : X, x0 \in x :: xs -> x0 \in ys
  Lem : exists xsl xsr : seq X, ys = xsl ++ [:: x] ++ xsr
  ============================
  size (x :: xs) <= size ys

----------------------------------------------------------------------------- *)

      move: Lem ⇒ [ysl [ysr EQ]]; subst ys.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 331)
  
  X : eqType
  m : nat
  IHm : forall xs ys : seq X,
        size ys <= m ->
        uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
  x : X
  xs, ysl, ysr : seq X
  SIZEm : size (ysl ++ [:: x] ++ ysr) <= m.+1
  UNIQ : uniq (x :: xs)
  SUB : forall x0 : X, x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
  ============================
  size (x :: xs) <= size (ysl ++ [:: x] ++ ysr)

----------------------------------------------------------------------------- *)

      rewrite !size_cat; simpl; rewrite -addnC add1n addSn ltnS -size_cat.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 371)
  
  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 xs <= size (ysr ++ ysl)

----------------------------------------------------------------------------- *)

      eapply IHm.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 372)
  
  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

subgoal 2 (ID 373) is:
 uniq xs
subgoal 3 (ID 374) is:
 forall x0 : X, x0 \in xs -> x0 \in ysr ++ ysl

----------------------------------------------------------------------------- *)

      - move: SIZEm; rewrite !size_cat; simpl; move ⇒ SIZE.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 399)
  
  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

subgoal 2 (ID 373) is:
 uniq xs
subgoal 3 (ID 374) is:
 forall x0 : X, x0 \in xs -> x0 \in ysr ++ ysl

----------------------------------------------------------------------------- *)

          by rewrite add1n addnS ltnS addnC in SIZE.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 373)
  
  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

subgoal 2 (ID 374) is:
 forall x0 : X, x0 \in xs -> x0 \in ysr ++ ysl

----------------------------------------------------------------------------- *)

      - by move: UNIQ; rewrite cons_uniq; move ⇒ /andP [_ UNIQ].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 374)
  
  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 x0 : X, x0 \in xs -> x0 \in ysr ++ ysl

----------------------------------------------------------------------------- *)

      - intros a IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 482)
  
  X : eqType
  m : nat
  IHm : forall xs ys : seq X,
        size ys <= m ->
        uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
  x : X
  xs, ysl, ysr : seq X
  SIZEm : size (ysl ++ [:: x] ++ ysr) <= m.+1
  UNIQ : uniq (x :: xs)
  SUB : forall x0 : X, x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
  a : X
  IN : a \in xs
  ============================
  a \in ysr ++ ysl

----------------------------------------------------------------------------- *)

        destruct (a == x) eqn: EQ.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 493)
  
  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

subgoal 2 (ID 494) is:
 a \in ysr ++ ysl

----------------------------------------------------------------------------- *)

        {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 493)
  
  X : eqType
  m : nat
  IHm : forall xs ys : seq X,
        size ys <= m ->
        uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
  x : X
  xs, ysl, ysr : seq X
  SIZEm : size (ysl ++ [:: x] ++ ysr) <= m.+1
  UNIQ : uniq (x :: xs)
  SUB : forall x0 : X, x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
  a : X
  IN : a \in xs
  EQ : (a == x) = true
  ============================
  a \in ysr ++ ysl

----------------------------------------------------------------------------- *)

exfalso.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 495)
  
  X : eqType
  m : nat
  IHm : forall xs ys : seq X,
        size ys <= m ->
        uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
  x : X
  xs, ysl, ysr : seq X
  SIZEm : size (ysl ++ [:: x] ++ ysr) <= m.+1
  UNIQ : uniq (x :: xs)
  SUB : forall x0 : X, x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
  a : X
  IN : a \in xs
  EQ : (a == x) = true
  ============================
  False

----------------------------------------------------------------------------- *)

          move: EQ UNIQ; rewrite cons_uniq; move ⇒ /eqP EQ /andP [NIN UNIQ].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 577)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 494)

subgoal 1 (ID 494) is:
 a \in ysr ++ ysl

----------------------------------------------------------------------------- *)

        }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 494)
  
  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

----------------------------------------------------------------------------- *)

        {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 494)
  
  X : eqType
  m : nat
  IHm : forall xs ys : seq X,
        size ys <= m ->
        uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
  x : X
  xs, ysl, ysr : seq X
  SIZEm : size (ysl ++ [:: x] ++ ysr) <= m.+1
  UNIQ : uniq (x :: xs)
  SUB : forall x0 : X, x0 \in x :: xs -> x0 \in ysl ++ [:: x] ++ ysr
  a : X
  IN : a \in xs
  EQ : (a == x) = false
  ============================
  a \in ysr ++ ysl

----------------------------------------------------------------------------- *)

specialize (SUB a).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 619)
  
  X : eqType
  m : nat
  IHm : forall xs ys : seq X,
        size ys <= m ->
        uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
  x : X
  xs, ysl, ysr : seq X
  SIZEm : size (ysl ++ [:: x] ++ ysr) <= m.+1
  UNIQ : uniq (x :: xs)
  a : X
  SUB : a \in x :: xs -> a \in ysl ++ [:: x] ++ ysr
  IN : a \in xs
  EQ : (a == x) = false
  ============================
  a \in ysr ++ ysl

----------------------------------------------------------------------------- *)

          feed SUB; first by rewrite in_cons; apply/orP; right.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 625)
  
  X : eqType
  m : nat
  IHm : forall xs ys : seq X,
        size ys <= m ->
        uniq xs -> (forall x : X, x \in xs -> x \in ys) -> size xs <= size ys
  x : X
  xs, ysl, ysr : seq X
  SIZEm : size (ysl ++ [:: x] ++ ysr) <= m.+1
  UNIQ : uniq (x :: xs)
  a : X
  SUB : a \in ysl ++ [:: x] ++ ysr
  IN : a \in xs
  EQ : (a == x) = false
  ============================
  a \in ysr ++ ysl

----------------------------------------------------------------------------- *)

          clear IN; move: SUB; rewrite !mem_cat; move ⇒ /orP [IN| /orP [IN|IN]].

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 766)
  
  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)

subgoal 2 (ID 767) is:
 (a \in ysr) || (a \in ysl)
subgoal 3 (ID 768) is:
 (a \in ysr) || (a \in ysl)

----------------------------------------------------------------------------- *)

          - by apply/orP; right.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 767)
  
  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)

subgoal 2 (ID 768) is:
 (a \in ysr) || (a \in ysl)

----------------------------------------------------------------------------- *)

          - exfalso.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 795)
  
  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]
  ============================
  False

subgoal 2 (ID 768) is:
 (a \in ysr) || (a \in ysl)

----------------------------------------------------------------------------- *)

              by move: IN; rewrite in_cons; move ⇒ /orP [IN|IN]; [rewrite IN in EQ | ].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 768)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

        }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

  (* We prove that if no element of a sequence [xs] satisfies
     a predicate [P], then [filter P xs] is equal to an empty
     sequence. *)
  Lemma filter_in_pred0:
    ∀ {X : eqType} (xs : seq X) P,
      (∀ x, x \in xs → ~~ P x) →
      filter P xs = [::].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 94)
  
  ============================
  forall (X : eqType) (xs : seq X) (P : X -> bool),
  (forall x : X, x \in xs -> ~~ P x) -> [seq x <- xs | P x] = [::]

----------------------------------------------------------------------------- *)

  Proof.
    intros X xs P F.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 98)
  
  X : eqType
  xs : seq X
  P : X -> bool
  F : forall x : X, x \in xs -> ~~ P x
  ============================
  [seq x <- xs | P x] = [::]

----------------------------------------------------------------------------- *)

    induction xs.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 107)
  
  X : eqType
  P : X -> bool
  F : forall x : X, x \in [::] -> ~~ P x
  ============================
  [seq x <- [::] | P x] = [::]

subgoal 2 (ID 114) is:
 [seq x <- a :: xs | P x] = [::]

----------------------------------------------------------------------------- *)

    - by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 114)
  
  X : eqType
  a : X
  xs : seq X
  P : X -> bool
  F : 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] = [::]

----------------------------------------------------------------------------- *)

    - simpl; rewrite IHxs; last first.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 122)
  
  X : eqType
  a : X
  xs : seq X
  P : X -> bool
  F : 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

subgoal 2 (ID 121) is:
 (if P a then [:: a] else [::]) = [::]

----------------------------------------------------------------------------- *)

      + intros; apply F.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 125)
  
  X : eqType
  a : X
  xs : seq X
  P : X -> bool
  F : forall x : X, x \in a :: xs -> ~~ P x
  IHxs : (forall x : X, x \in xs -> ~~ P x) -> [seq x <- xs | P x] = [::]
  x : X
  H : x \in xs
  ============================
  x \in a :: xs

subgoal 2 (ID 121) is:
 (if P a then [:: a] else [::]) = [::]

----------------------------------------------------------------------------- *)

          by rewrite in_cons; apply/orP; right.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 121)
  
  X : eqType
  a : X
  xs : seq X
  P : X -> bool
  F : 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 [::]) = [::]

----------------------------------------------------------------------------- *)

      + destruct (P a) eqn:EQ; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 169)
  
  X : eqType
  a : X
  xs : seq X
  P : X -> bool
  F : 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] = [::]

----------------------------------------------------------------------------- *)

        move: EQ ⇒ /eqP; rewrite eqb_id -[P a]Bool.negb_involutive; move ⇒ /negP T.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 262)
  
  X : eqType
  a : X
  xs : seq X
  P : X -> bool
  F : 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] = [::]

----------------------------------------------------------------------------- *)

        exfalso; apply: T.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 269)
  
  X : eqType
  a : X
  xs : seq X
  P : X -> bool
  F : 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 F; apply/orP; left.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

We show that any two elements having the same index in a unique sequence must be equal.
  Lemma eq_ind_in_seq:
    ∀ (T : eqType) a b (xs : seq T),
      index a xs = index b xs →
      uniq xs →
      a \in xs →
      b \in xs →
      a = b.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 114)
  
  ============================
  forall (T : eqType) (a b : T) (xs : seq T),
  index a xs = index b xs -> uniq xs -> a \in xs -> b \in xs -> a = b

----------------------------------------------------------------------------- *)

  Proof.
    move⇒ T a b xs EQ UNIQ IN_a IN_b.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 122)
  
  T : eqType
  a, b : T
  xs : seq T
  EQ : index a xs = index b xs
  UNIQ : uniq xs
  IN_a : a \in xs
  IN_b : b \in xs
  ============================
  a = b

----------------------------------------------------------------------------- *)

    move: (nth_index a IN_a) ⇒ EQ_a.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 127)
  
  T : eqType
  a, b : T
  xs : seq T
  EQ : index a xs = index b xs
  UNIQ : uniq xs
  IN_a : a \in xs
  IN_b : b \in xs
  EQ_a : nth a xs (index a xs) = a
  ============================
  a = b

----------------------------------------------------------------------------- *)

    move: (nth_index a IN_b) ⇒ EQ_b.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 132)
  
  T : eqType
  a, b : T
  xs : seq T
  EQ : index a xs = index b xs
  UNIQ : uniq 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

----------------------------------------------------------------------------- *)

    now rewrite -EQ_a -EQ_b EQ.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

We show that the nth element in a sequence lies in the sequence or is the default element.
  Lemma default_or_in:
    ∀ (T : eqType) (n : nat) (d : T) (xs : seq T),
      nth d xs n = d ∨ nth d xs n \in xs.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 123)
  
  ============================
  forall (T : eqType) (n : nat) (d : T) (xs : seq T),
  nth d xs n = d \/ nth d xs n \in xs

----------------------------------------------------------------------------- *)

  Proof.
    clear; intros.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 127)
  
  T : eqType
  n : nat
  d : T
  xs : seq T
  ============================
  nth d xs n = d \/ nth d xs n \in xs

----------------------------------------------------------------------------- *)

    destruct (leqP (size xs) n).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 151)
  
  T : eqType
  n : nat
  d : T
  xs : seq T
  i : size xs <= n
  ============================
  nth d xs n = d \/ nth d xs n \in xs

subgoal 2 (ID 152) is:
 nth d xs n = d \/ nth d xs n \in xs

----------------------------------------------------------------------------- *)

    - now left; apply nth_default.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 152)
  
  T : eqType
  n : nat
  d : T
  xs : seq T
  i : n < size xs
  ============================
  nth d xs n = d \/ nth d xs n \in xs

----------------------------------------------------------------------------- *)

    - now right; apply mem_nth.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

We show that in a unique sequence of size greater than one there exist two unique elements.
  Lemma exists_two:
    ∀ (T : eqType) (xs : seq T),
      size xs > 1 →
      uniq xs →
      ∃ a b, a ≠ b ∧ a \in xs ∧ b \in xs.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 143)
  
  ============================
  forall (T : eqType) (xs : seq T),
  1 < size xs -> uniq xs -> exists a b : T, a <> b /\ a \in xs /\ b \in xs

----------------------------------------------------------------------------- *)

  Proof.
    move⇒ T xs GT1 UNIQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 147)
  
  T : eqType
  xs : seq T
  GT1 : 1 < size xs
  UNIQ : uniq xs
  ============================
  exists a b : T, a <> b /\ a \in xs /\ b \in xs

----------------------------------------------------------------------------- *)

    (* get an element of [T] so that we can use nth *)
    have HEAD: ∃ x, ohead xs = Some x
        by elim: xs GT1 UNIQ ⇒ // a l _ _ _; ∃ a ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 247)
  
  T : eqType
  xs : seq T
  GT1 : 1 < size xs
  UNIQ : uniq xs
  HEAD : exists x : T, ohead xs = Some x
  ============================
  exists a b : T, a <> b /\ a \in xs /\ b \in xs

----------------------------------------------------------------------------- *)

    move: (HEAD) ⇒ [x0 _].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 260)
  
  T : eqType
  xs : seq T
  GT1 : 1 < size xs
  UNIQ : uniq xs
  HEAD : exists x : T, ohead xs = Some x
  x0 : T
  ============================
  exists a b : T, a <> b /\ a \in xs /\ b \in xs

----------------------------------------------------------------------------- *)

    have GT0: 0 < size xs by apply ltn_trans with (n := 1).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 266)
  
  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

----------------------------------------------------------------------------- *)

    ∃ (nth x0 xs 0).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 269)
  
  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

----------------------------------------------------------------------------- *)

    ∃ (nth x0 xs 1).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 272)
  
  T : eqType
  xs : seq T
  GT1 : 1 < size xs
  UNIQ : uniq xs
  HEAD : exists x : T, ohead xs = Some x
  x0 : T
  GT0 : 0 < size xs
  ============================
  nth x0 xs 0 <> nth x0 xs 1 /\ nth x0 xs 0 \in xs /\ nth x0 xs 1 \in xs

----------------------------------------------------------------------------- *)

    repeat split; try apply mem_nth ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 274)
  
  T : eqType
  xs : seq T
  GT1 : 1 < size xs
  UNIQ : uniq xs
  HEAD : exists x : T, ohead xs = Some x
  x0 : T
  GT0 : 0 < size xs
  ============================
  nth x0 xs 0 <> nth x0 xs 1

----------------------------------------------------------------------------- *)

    apply /eqP; apply contraNneq with (b := (0 == 1)) ⇒ // /eqP.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 437)
  
  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

----------------------------------------------------------------------------- *)

    now rewrite nth_uniq.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

End AdditionalLemmas.

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

Additional lemmas about [rem_all] for lists.
Section RemAllList.

First we prove that [x ∉ rem_all x xs].
  Lemma nin_rem_all:
    ∀ {X : eqType} (x : X) (xs : seq X),
      ¬ (x \in rem_all x xs).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 42)
  
  ============================
  forall (X : eqType) (x : X) (xs : seq X), ~ x \in rem_all x xs

----------------------------------------------------------------------------- *)

  Proof.
    intros ? ? ? IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 47)
  
  X : eqType
  x : X
  xs : seq X
  IN : x \in rem_all x xs
  ============================
  False

----------------------------------------------------------------------------- *)

    induction xs.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 56)
  
  X : eqType
  x : X
  IN : x \in rem_all x [::]
  ============================
  False

subgoal 2 (ID 61) is:
 False

----------------------------------------------------------------------------- *)

    - by simpl in IN.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 61)
  
  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

----------------------------------------------------------------------------- *)

    - apply IHxs.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 92)
  
  X : eqType
  x, a : X
  xs : seq X
  IN : x \in rem_all x (a :: xs)
  IHxs : x \in rem_all x xs -> False
  ============================
  x \in rem_all x xs

----------------------------------------------------------------------------- *)

      simpl in IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 95)
  
  X : eqType
  x, a : X
  xs : seq X
  IN : x \in (if a == x then rem_all x xs else a :: rem_all x xs)
  IHxs : x \in rem_all x xs -> False
  ============================
  x \in rem_all x xs

----------------------------------------------------------------------------- *)

      destruct (a == x) eqn:EQ; first by done.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 119)
  
  X : eqType
  x, a : X
  xs : seq X
  EQ : (a == x) = false
  IN : x \in a :: rem_all x xs
  IHxs : x \in rem_all x xs -> False
  ============================
  x \in rem_all x xs

----------------------------------------------------------------------------- *)

      move: IN; rewrite in_cons; move ⇒ /orP [/eqP EQ2 | IN]; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 202)
  
  X : eqType
  x, a : X
  xs : seq X
  EQ : (a == x) = false
  IHxs : x \in rem_all x xs -> False
  EQ2 : x = a
  ============================
  x \in rem_all x xs

----------------------------------------------------------------------------- *)

      subst; exfalso.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 212)
  
  X : eqType
  a : X
  xs : seq X
  IHxs : a \in rem_all a xs -> False
  EQ : (a == a) = false
  ============================
  False

----------------------------------------------------------------------------- *)

        by rewrite eq_refl in EQ.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Next we show that [rem_all x xs ⊆ xs].
  Lemma in_rem_all:
    ∀ {X : eqType} (a x : X) (xs : seq X),
      a \in rem_all x xs → a \in xs.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 52)
  
  ============================
  forall (X : eqType) (a x : X) (xs : seq X), a \in rem_all x xs -> a \in xs

----------------------------------------------------------------------------- *)

  Proof.
    intros X a x xs IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 57)
  
  X : eqType
  a, x : X
  xs : seq X
  IN : a \in rem_all x xs
  ============================
  a \in xs

----------------------------------------------------------------------------- *)

    induction xs.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 66)
  
  X : eqType
  a, x : X
  IN : a \in rem_all x [::]
  ============================
  a \in [::]

subgoal 2 (ID 71) is:
 a \in a0 :: xs

----------------------------------------------------------------------------- *)

    - by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 71)
  
  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

----------------------------------------------------------------------------- *)

    - simpl in IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 74)
  
  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

----------------------------------------------------------------------------- *)

      destruct (a0 == x) eqn:EQ.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 94)
  
  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

subgoal 2 (ID 98) is:
 a \in a0 :: xs

----------------------------------------------------------------------------- *)

      + by rewrite in_cons; apply/orP; right; eauto.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 98)
  
  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

----------------------------------------------------------------------------- *)

      + move: IN; rewrite in_cons; move ⇒ /orP [EQ2|IN].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 186)
  
  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

subgoal 2 (ID 187) is:
 a \in a0 :: xs

----------------------------------------------------------------------------- *)

        × by rewrite in_cons; apply/orP; left.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 187)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

If an element [x1] is smaller than any element of a sequence [xs], then [rem_all x xs = xs].
  Lemma rem_lt_id:
    ∀ x xs,
      (∀ y, y \in xs → x < y) →
      rem_all x xs = xs.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

  Proof.
    intros ? ? MIN; induction xs.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 80)
  
  x : nat
  MIN : forall y : nat, y \in [::] -> x < y
  ============================
  rem_all x [::] = [::]

subgoal 2 (ID 85) is:
 rem_all x (a :: xs) = a :: xs

----------------------------------------------------------------------------- *)

    - by simpl.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 85)
  
  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

----------------------------------------------------------------------------- *)

    - simpl.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 93)
  
  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
  ============================
  (if a == x then rem_all x xs else a :: rem_all x xs) = a :: xs

----------------------------------------------------------------------------- *)

      have → : (a == x) = false.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 97)
  
  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

subgoal 2 (ID 102) is:
 a :: rem_all x xs = a :: xs

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 97)
  
  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

----------------------------------------------------------------------------- *)

apply/eqP/eqP; rewrite neq_ltn; apply/orP; right.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 270)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 102)

subgoal 1 (ID 102) is:
 a :: rem_all x xs = a :: xs

----------------------------------------------------------------------------- *)

      }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 102)
  
  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

----------------------------------------------------------------------------- *)

      rewrite IHxs //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 307)
  
  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

----------------------------------------------------------------------------- *)

      intros; apply: MIN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 344)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  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 prove that [index_iota a b = a :: index_iota a.+1 b] for [a < b].
  Remark index_iota_lt_step:
    ∀ a b,
      a < b →
      index_iota a b = a :: index_iota a.+1 b.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 42)
  
  ============================
  forall a b : nat, a < b -> index_iota a b = a :: index_iota a.+1 b

----------------------------------------------------------------------------- *)

  Proof.
    intros ? ? LT; unfold index_iota.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

    destruct b; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

    rewrite ltnS in LT.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

      by rewrite subSn //.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

We prove that one can remove duplicating element from the head of a sequence by which [range] is filtered.
  Lemma range_filter_2cons:
    ∀ x xs k,
      [seq ρ <- range 0 k | ρ \in x :: x :: xs] =
      [seq ρ <- range 0 k | ρ \in x :: xs].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 68)
  
  ============================
  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]

----------------------------------------------------------------------------- *)

  Proof.
    intros.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

    apply eq_filter; intros ?.

(* ----------------------------------[ coqtop ]---------------------------------

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

----------------------------------------------------------------------------- *)

    repeat rewrite in_cons.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 86)
  
  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).

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Consider [a], [b], and [x] s.t. [a ≤ x < b], then filter of [iota_index a b] with predicate [(? == x)] yields [::x].
  Lemma index_iota_filter_eqx:
    ∀ x a b,
      a ≤ x < b →
      [seq ρ <- index_iota a b | ρ == x] = [::x].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 80)
  
  ============================
  forall x a b : nat,
  a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

  Proof.
    intros ? ? ?.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 83)
  
  x, a, b : nat
  ============================
  a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

    have EX : ∃ k, b - a ≤ k.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 86)
  
  x, a, b : nat
  ============================
  exists k : nat, b - a <= k

subgoal 2 (ID 88) is:
 a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 86)
  
  x, a, b : nat
  ============================
  exists k : nat, b - a <= k

----------------------------------------------------------------------------- *)

∃ (b-a); now simpl.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 88)

subgoal 1 (ID 88) is:
 a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

}
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 88)
  
  x, a, b : nat
  EX : exists k : nat, b - a <= k
  ============================
  a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

destruct EX as [k BO].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 97)
  
  x, a, b, k : nat
  BO : b - a <= k
  ============================
  a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

    revert x a b BO.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 99)
  
  k : nat
  ============================
  forall x a b : nat,
  b - a <= k -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

    induction k.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 103)
  
  ============================
  forall x a b : nat,
  b - a <= 0 -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]

subgoal 2 (ID 106) is:
 forall x a b : nat,
 b - a <= k.+1 -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 103)
  
  ============================
  forall x a b : nat,
  b - a <= 0 -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

move ⇒ x a b BO /andP [GE LT]; exfalso.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 151)
  
  x, a, b : nat
  BO : b - a <= 0
  GE : a <= x
  LT : x < b
  ============================
  False

----------------------------------------------------------------------------- *)

      move: BO; rewrite leqn0 subn_eq0; move ⇒ BO.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 161)
  
  x, a, b : nat
  GE : a <= x
  LT : x < b
  BO : b <= a
  ============================
  False

----------------------------------------------------------------------------- *)

        by ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 106)

subgoal 1 (ID 106) is:
 forall x a b : nat,
 b - a <= k.+1 -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

    }
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 106)
  
  k : nat
  IHk : forall x a b : nat,
        b - a <= k ->
        a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
  ============================
  forall x a b : nat,
  b - a <= k.+1 -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 106)
  
  k : nat
  IHk : forall x a b : nat,
        b - a <= k ->
        a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
  ============================
  forall x a b : nat,
  b - a <= k.+1 -> a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

move ⇒ x a b BO /andP [GE LT].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 387)
  
  k : nat
  IHk : forall x a b : nat,
        b - a <= k ->
        a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
  x, a, b : nat
  BO : b - a <= k.+1
  GE : a <= x
  LT : x < b
  ============================
  [seq ρ <- index_iota a b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

      destruct a.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 401)
  
  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]

subgoal 2 (ID 407) is:
 [seq ρ <- index_iota a.+1 b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 401)
  
  k : nat
  IHk : forall x a b : nat,
        b - a <= k ->
        a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
  x, b : nat
  BO : b - 0 <= k.+1
  GE : 0 <= x
  LT : x < b
  ============================
  [seq ρ <- index_iota 0 b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

destruct b; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 425)
  
  k : nat
  IHk : forall x a b : nat,
        b - a <= k ->
        a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
  x, b : nat
  BO : b.+1 - 0 <= k.+1
  GE : 0 <= x
  LT : x < b.+1
  ============================
  [seq ρ <- index_iota 0 b.+1 | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

        rewrite index_iota_lt_step //; simpl.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 483)
  
  k : nat
  IHk : forall x a b : nat,
        b - a <= k ->
        a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
  x, b : nat
  BO : b.+1 - 0 <= k.+1
  GE : 0 <= x
  LT : x < b.+1
  ============================
  (if 0 == x
   then 0 :: [seq ρ <- index_iota 1 b.+1 | ρ == x]
   else [seq ρ <- index_iota 1 b.+1 | ρ == x]) = [:: x]

----------------------------------------------------------------------------- *)

        destruct (0 == x) eqn:EQ.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 496)
  
  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]

subgoal 2 (ID 497) is:
 [seq ρ <- index_iota 1 b.+1 | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

        - move: EQ ⇒ /eqP EQ; subst x.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 541)
  
  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]

subgoal 2 (ID 497) is:
 [seq ρ <- index_iota 1 b.+1 | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

          rewrite filter_in_pred0 //.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 549)
  
  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

subgoal 2 (ID 497) is:
 [seq ρ <- index_iota 1 b.+1 | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

            by intros x; rewrite mem_index_iota -lt0n; move ⇒ /andP [T1 _].
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 497)
  
  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; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 407)

subgoal 1 (ID 407) is:
 [seq ρ <- index_iota a.+1 b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

      }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 407)
  
  k : nat
  IHk : forall x a b : nat,
        b - a <= k ->
        a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
  x, a, b : nat
  BO : b - a.+1 <= k.+1
  GE : a < x
  LT : x < b
  ============================
  [seq ρ <- index_iota a.+1 b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

      rewrite index_iota_lt_step; last by ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2645)
  
  k : nat
  IHk : forall x a b : nat,
        b - a <= k ->
        a <= x < b -> [seq ρ <- index_iota a b | ρ == x] = [:: x]
  x, a, b : nat
  BO : b - a.+1 <= k.+1
  GE : a < x
  LT : x < b
  ============================
  [seq ρ <- a.+1 :: index_iota a.+2 b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

      simpl; destruct (a.+1 == x) eqn:EQ.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 3463)
  
  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]

subgoal 2 (ID 3464) is:
 [seq ρ <- index_iota a.+2 b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

      - move: EQ ⇒ /eqP EQ; subst x.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 3508)
  
  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]

subgoal 2 (ID 3464) is:
 [seq ρ <- index_iota a.+2 b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

        rewrite filter_in_pred0 //.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 3516)
  
  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

subgoal 2 (ID 3464) is:
 [seq ρ <- index_iota a.+2 b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

        intros x; rewrite mem_index_iota; move ⇒ /andP [T1 _].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 3588)
  
  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

subgoal 2 (ID 3464) is:
 [seq ρ <- index_iota a.+2 b | ρ == x] = [:: x]

----------------------------------------------------------------------------- *)

          by rewrite neq_ltn; apply/orP; right.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 3464)
  
  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 //; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    }
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

As a corollary we prove that filter of [iota_index a b] with predicate [(_ ∈ [::x])] yields [::x].
  Corollary index_iota_filter_singl:
    ∀ x a b,
      a ≤ x < b →
      [seq ρ <- index_iota a b | ρ \in [:: x]] = [::x].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 97)
  
  ============================
  forall x a b : nat,
  a <= x < b -> [seq ρ <- index_iota a b | ρ \in [:: x]] = [:: x]

----------------------------------------------------------------------------- *)

  Proof.
    intros ? ? ? NEQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 101)
  
  x, a, b : nat
  NEQ : a <= x < b
  ============================
  [seq ρ <- index_iota a b | ρ \in [:: x]] = [:: x]

----------------------------------------------------------------------------- *)

    rewrite -{2}(index_iota_filter_eqx _ a b) //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 108)
  
  x, a, b : nat
  NEQ : a <= x < b
  ============================
  [seq ρ <- index_iota a b | ρ \in [:: x]] =
  [seq ρ <- index_iota a b | ρ == x]

----------------------------------------------------------------------------- *)

    apply eq_filter; intros ?.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 134)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Next we prove that if an element [x] is not in a sequence [xs], then [iota_index a b] filtered with predicate [(_ ∈ xs)] is equal to [iota_index a b] filtered with predicate [(_ ∈ rem_all x xs)].
  Lemma index_iota_filter_inxs:
    ∀ a b x xs,
      x < a →
      [seq ρ <- index_iota a b | ρ \in xs] =
      [seq ρ <- index_iota a b | ρ \in rem_all x xs].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 123)
  
  ============================
  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]

----------------------------------------------------------------------------- *)

  Proof.
    intros a b x xs LT.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 128)
  
  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]

----------------------------------------------------------------------------- *)

    apply eq_in_filter.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 129)
  
  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)}

----------------------------------------------------------------------------- *)

    intros y; rewrite mem_index_iota; move ⇒ /andP [LE GT].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 176)
  
  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)

----------------------------------------------------------------------------- *)

    induction xs as [ | y' xs]; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 186)
  
  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))

----------------------------------------------------------------------------- *)

    rewrite in_cons IHxs; simpl; clear IHxs.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 199)
  
  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))

----------------------------------------------------------------------------- *)

    destruct (y == y') eqn:EQ1, (y' == x) eqn:EQ2; auto.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 226)
  
  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)

subgoal 2 (ID 227) is:
 true || (y \in rem_all x xs) = (y \in y' :: rem_all x xs)
subgoal 3 (ID 241) is:
 false || (y \in rem_all x xs) = (y \in y' :: rem_all x xs)

----------------------------------------------------------------------------- *)

    - exfalso.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 245)
  
  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
  ============================
  False

subgoal 2 (ID 227) is:
 true || (y \in rem_all x xs) = (y \in y' :: rem_all x xs)
subgoal 3 (ID 241) is:
 false || (y \in rem_all x xs) = (y \in y' :: rem_all x xs)

----------------------------------------------------------------------------- *)

      move: EQ1 EQ2 ⇒ /eqP EQ1 /eqP EQ2; subst.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 332)
  
  a, b, x : nat
  xs : seq nat_eqType
  LT : x < a
  LE : a <= x
  GT : x < b
  ============================
  False

subgoal 2 (ID 227) is:
 true || (y \in rem_all x xs) = (y \in y' :: rem_all x xs)
subgoal 3 (ID 241) is:
 false || (y \in rem_all x xs) = (y \in y' :: rem_all x xs)

----------------------------------------------------------------------------- *)

        by ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 227)
  
  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)

subgoal 2 (ID 241) is:
 false || (y \in rem_all x xs) = (y \in y' :: rem_all x xs)

----------------------------------------------------------------------------- *)

    - move: EQ1 ⇒ /eqP EQ1; subst.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 557)
  
  a, b, x : nat
  y' : nat_eqType
  xs : seq nat_eqType
  LT : x < a
  GT : y' < b
  LE : a <= y'
  EQ2 : (y' == x) = false
  ============================
  true || (y' \in rem_all x xs) = (y' \in y' :: rem_all x xs)

subgoal 2 (ID 241) is:
 false || (y \in rem_all x xs) = (y \in y' :: rem_all x xs)

----------------------------------------------------------------------------- *)

        by rewrite in_cons eq_refl.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 241)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

We prove that if an element [x] is a min of a sequence [xs], then [iota_index a b] filtered with predicate [(_ ∈ x::xs)] is equal to [x :: iota_index a b] filtered with predicate [(_ ∈ rem_all x xs)].
  Lemma index_iota_filter_step:
    ∀ x xs a b,
      a ≤ x < b →
      (∀ y, y \in xs → x ≤ y) →
      [seq ρ <- index_iota a b | ρ \in x :: xs] =
      x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 157)
  
  ============================
  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]

----------------------------------------------------------------------------- *)

  Proof.
    intros x xs a b B MIN.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 163)
  
  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]

----------------------------------------------------------------------------- *)

    have EX : ∃ k, b - a ≤ k.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 166)
  
  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

subgoal 2 (ID 168) is:
 [seq ρ <- index_iota a b | ρ \in x :: xs] =
 x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 166)
  
  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

----------------------------------------------------------------------------- *)

∃ (b-a); now simpl.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 168)

subgoal 1 (ID 168) is:
 [seq ρ <- index_iota a b | ρ \in x :: xs] =
 x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]

----------------------------------------------------------------------------- *)

}
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 168)
  
  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]

----------------------------------------------------------------------------- *)

destruct EX as [k BO].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 177)
  
  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]

----------------------------------------------------------------------------- *)

    revert x xs a b B MIN BO.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 179)
  
  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]

----------------------------------------------------------------------------- *)

    induction k; move ⇒ x xs a b /andP [LE GT] MIN BO.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 232)
  
  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]

subgoal 2 (ID 278) is:
 [seq ρ <- index_iota a b | ρ \in x :: xs] =
 x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]

----------------------------------------------------------------------------- *)

    - by move_neq_down BO; ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 278)
  
  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]

----------------------------------------------------------------------------- *)

    - move: LE; rewrite leq_eqVlt; move ⇒ /orP [/eqP EQ|LT].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 596)
  
  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]

subgoal 2 (ID 597) is:
 [seq ρ <- index_iota a b | ρ \in x :: xs] =
 x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]

----------------------------------------------------------------------------- *)

      + subst.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 603)
  
  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]

subgoal 2 (ID 597) is:
 [seq ρ <- index_iota a b | ρ \in x :: xs] =
 x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]

----------------------------------------------------------------------------- *)

        rewrite index_iota_lt_step //.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 608)
  
  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]

subgoal 2 (ID 597) is:
 [seq ρ <- index_iota a b | ρ \in x :: xs] =
 x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]

----------------------------------------------------------------------------- *)

        replace ([seq ρ <- x :: index_iota x.+1 b | ρ \in x :: xs])
          with (x :: [seq ρ <- index_iota x.+1 b | ρ \in x :: xs]); last first.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 651)
  
  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]

subgoal 2 (ID 653) is:
 x :: [seq ρ <- index_iota x.+1 b | ρ \in x :: xs] =
 x :: [seq ρ <- x :: index_iota x.+1 b | ρ \in rem_all x xs]
subgoal 3 (ID 597) is:
 [seq ρ <- index_iota a b | ρ \in x :: xs] =
 x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]

----------------------------------------------------------------------------- *)

        {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 651)
  
  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]

----------------------------------------------------------------------------- *)

simpl; replace (@in_mem nat x (@mem nat (seq_predType nat_eqType) (x::xs))) with true.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 664)
  
  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]

subgoal 2 (ID 662) is:
 true = (x \in x :: xs)

----------------------------------------------------------------------------- *)

          all: by auto; rewrite in_cons eq_refl.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 653)

subgoal 1 (ID 653) is:
 x :: [seq ρ <- index_iota x.+1 b | ρ \in x :: xs] =
 x :: [seq ρ <- x :: index_iota x.+1 b | ρ \in rem_all x xs]
subgoal 2 (ID 597) is:
 [seq ρ <- index_iota a b | ρ \in x :: xs] =
 x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]

----------------------------------------------------------------------------- *)

        }

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 653)
  
  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]

subgoal 2 (ID 597) is:
 [seq ρ <- index_iota a b | ρ \in x :: xs] =
 x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]

----------------------------------------------------------------------------- *)

        rewrite (index_iota_filter_inxs _ _ x) //; simpl.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 717)
  
  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])

subgoal 2 (ID 597) is:
 [seq ρ <- index_iota a b | ρ \in x :: xs] =
 x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]

----------------------------------------------------------------------------- *)

        rewrite eq_refl.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 721)
  
  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])

subgoal 2 (ID 597) is:
 [seq ρ <- index_iota a b | ρ \in x :: xs] =
 x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]

----------------------------------------------------------------------------- *)

        replace (@in_mem nat x (@mem nat (seq_predType nat_eqType) (@rem_all nat_eqType x xs))) with false; last first.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 723)
  
  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)

subgoal 2 (ID 725) is:
 x :: [seq ρ <- index_iota x.+1 b | ρ \in rem_all x xs] =
 x :: [seq ρ <- index_iota x.+1 b | ρ \in rem_all x xs]
subgoal 3 (ID 597) is:
 [seq ρ <- index_iota a b | ρ \in x :: xs] =
 x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]

----------------------------------------------------------------------------- *)

        apply/eqP; rewrite eq_sym eqbF_neg.
(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 789)
  
  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

subgoal 2 (ID 725) is:
 x :: [seq ρ <- index_iota x.+1 b | ρ \in rem_all x xs] =
 x :: [seq ρ <- index_iota x.+1 b | ρ \in rem_all x xs]
subgoal 3 (ID 597) is:
 [seq ρ <- index_iota a b | ρ \in x :: xs] =
 x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]

----------------------------------------------------------------------------- *)

apply/negP; apply nin_rem_all.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 725)
  
  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]

subgoal 2 (ID 597) is:
 [seq ρ <- index_iota a b | ρ \in x :: xs] =
 x :: [seq ρ <- index_iota a b | ρ \in rem_all x xs]

----------------------------------------------------------------------------- *)

        reflexivity.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 597)
  
  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]

----------------------------------------------------------------------------- *)

      + rewrite index_iota_lt_step //; last by ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 816)
  
  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]

----------------------------------------------------------------------------- *)

        replace ([seq ρ <- a :: index_iota a.+1 b | ρ \in x :: xs])
          with ([seq ρ <- index_iota a.+1 b | ρ \in x :: xs]); last first.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1682)
  
  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]

subgoal 2 (ID 1684) is:
 [seq ρ <- index_iota a.+1 b | ρ \in x :: xs] =
 x :: [seq ρ <- a :: index_iota a.+1 b | ρ \in rem_all x xs]

----------------------------------------------------------------------------- *)

        {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1682)
  
  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]

----------------------------------------------------------------------------- *)

simpl; replace (@in_mem nat a (@mem nat (seq_predType nat_eqType) (@cons nat x xs))) with false; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1692)
  
  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)

----------------------------------------------------------------------------- *)

          apply/eqP; rewrite eq_sym eqbF_neg.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1758)
  
  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

----------------------------------------------------------------------------- *)

          apply/negP; rewrite in_cons; intros C; move: C ⇒ /orP [/eqP C|C].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1863)
  
  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

subgoal 2 (ID 1864) is:
 False

----------------------------------------------------------------------------- *)

          - by subst; rewrite ltnn in LT.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1864)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1684)

subgoal 1 (ID 1684) is:
 [seq ρ <- index_iota a.+1 b | ρ \in x :: xs] =
 x :: [seq ρ <- a :: index_iota a.+1 b | ρ \in rem_all x xs]

----------------------------------------------------------------------------- *)

        }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1684)
  
  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]

----------------------------------------------------------------------------- *)

        replace ([seq ρ <- a :: index_iota a.+1 b | ρ \in rem_all x xs])
          with ([seq ρ <- index_iota a.+1 b | ρ \in rem_all x xs]); last first.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1978)
  
  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]

subgoal 2 (ID 1980) is:
 [seq ρ <- index_iota a.+1 b | ρ \in x :: xs] =
 x :: [seq ρ <- index_iota a.+1 b | ρ \in rem_all x xs]

----------------------------------------------------------------------------- *)

        {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1978)
  
  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]

----------------------------------------------------------------------------- *)

simpl; replace (@in_mem nat a (@mem nat (seq_predType nat_eqType) (@rem_all nat_eqType x xs))) with false; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1987)
  
  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)

----------------------------------------------------------------------------- *)

          apply/eqP; rewrite eq_sym eqbF_neg; apply/negP; intros C.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2075)
  
  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

----------------------------------------------------------------------------- *)

          apply in_rem_all in C.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 2077)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1980)

subgoal 1 (ID 1980) is:
 [seq ρ <- index_iota a.+1 b | ρ \in x :: xs] =
 x :: [seq ρ <- index_iota a.+1 b | ρ \in rem_all x xs]

----------------------------------------------------------------------------- *)

        }
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1980)
  
  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 //; ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

For convenience, we define a special case of lemma [index_iota_filter_step] for [a = 0] and [b = k.+1].
  Corollary range_iota_filter_step:
    ∀ x xs k,
      x ≤ k →
      (∀ y, y \in xs → x ≤ y) →
      [seq ρ <- range 0 k | ρ \in x :: xs] =
      x :: [seq ρ <- range 0 k | ρ \in rem_all x xs].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 190)
  
  ============================
  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]

----------------------------------------------------------------------------- *)

  Proof.
    intros x xs k LE MIN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 195)
  
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

We prove that if [x < a], then [x < (filter P (index_iota a b))[idx]] for any predicate [P].
  Lemma iota_filter_gt:
    ∀ x a b idx P,
      x < a →
      idx < size ([seq x <- index_iota a b | P x]) →
      x < nth 0 [seq x <- index_iota a b | P x] idx.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 205)
  
  ============================
  forall (x a b idx : nat) (P : nat -> bool),
  x < a ->
  idx < size [seq x0 <- index_iota a b | P x0] ->
  x < nth 0 [seq x0 <- index_iota a b | P x0] idx

----------------------------------------------------------------------------- *)

  Proof.
    clear; intros ? ? ? ? ?.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 210)
  
  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

----------------------------------------------------------------------------- *)

    have EX : ∃ k, b - a ≤ k.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 213)
  
  x, a, b, idx : nat
  P : nat -> bool
  ============================
  exists k : nat, b - a <= k

subgoal 2 (ID 215) is:
 x < a ->
 idx < size [seq x0 <- index_iota a b | P x0] ->
 x < nth 0 [seq x0 <- index_iota a b | P x0] idx

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 213)
  
  x, a, b, idx : nat
  P : nat -> bool
  ============================
  exists k : nat, b - a <= k

----------------------------------------------------------------------------- *)

∃ (b-a); now simpl.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 215)

subgoal 1 (ID 215) is:
 x < a ->
 idx < size [seq x0 <- index_iota a b | P x0] ->
 x < nth 0 [seq x0 <- index_iota a b | P x0] idx

----------------------------------------------------------------------------- *)

}
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 215)
  
  x, a, b, idx : nat
  P : nat -> bool
  EX : exists k : nat, 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

----------------------------------------------------------------------------- *)

destruct EX as [k BO].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 224)
  
  x, a, b, idx : nat
  P : nat -> bool
  k : nat
  BO : 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

----------------------------------------------------------------------------- *)

    revert x a b idx P BO; induction k.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 230)
  
  ============================
  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

subgoal 2 (ID 233) is:
 forall (x a b idx : nat) (P : nat -> bool),
 b - a <= k.+1 ->
 x < a ->
 idx < size [seq x0 <- index_iota a b | P x0] ->
 x < nth 0 [seq x0 <- index_iota a b | P x0] idx

----------------------------------------------------------------------------- *)

    - move ⇒ x a b idx P BO LT1 LT2.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 241)
  
  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 x0 <- index_iota a b | P x0] idx

subgoal 2 (ID 233) is:
 forall (x a b idx : nat) (P : nat -> bool),
 b - a <= k.+1 ->
 x < a ->
 idx < size [seq x0 <- index_iota a b | P x0] ->
 x < nth 0 [seq x0 <- index_iota a b | P x0] idx

----------------------------------------------------------------------------- *)

      move: BO; rewrite leqn0; move ⇒ /eqP BO.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 280)
  
  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 x0 <- index_iota a b | P x0] idx

subgoal 2 (ID 233) is:
 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

----------------------------------------------------------------------------- *)

        by rewrite /index_iota BO in LT2; simpl in LT2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 233)
  
  k : nat
  IHk : forall (x a b idx : nat) (P : nat -> bool),
        b - a <= k ->
        x < a ->
        idx < size [seq x0 <- index_iota a b | P x0] ->
        x < nth 0 [seq x0 <- index_iota a b | P x0] idx
  ============================
  forall (x a b idx : nat) (P : nat -> bool),
  b - a <= k.+1 ->
  x < a ->
  idx < size [seq x0 <- index_iota a b | P x0] ->
  x < nth 0 [seq x0 <- index_iota a b | P x0] idx

----------------------------------------------------------------------------- *)

    - move ⇒ x a b idx P BO LT1 LT2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 333)
  
  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 x0 <- index_iota a b | P x0] idx

----------------------------------------------------------------------------- *)

      case: (leqP b a) ⇒ [N|N].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 345)
  
  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 x0 <- index_iota a b | P x0] idx

subgoal 2 (ID 346) is:
 x < nth 0 [seq x0 <- index_iota a b | P x0] idx

----------------------------------------------------------------------------- *)

      + move: N; rewrite -subn_eq0; move ⇒ /eqP EQ.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 386)
  
  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 x0 <- index_iota a b | P x0] idx

subgoal 2 (ID 346) is:
 x < nth 0 [seq x0 <- index_iota a b | P x0] idx

----------------------------------------------------------------------------- *)

          by rewrite /index_iota EQ //= in LT2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 346)
  
  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 x0 <- index_iota a b | P x0] idx

----------------------------------------------------------------------------- *)

      + rewrite index_iota_lt_step; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 427)
  
  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 x0 <- a :: index_iota a.+1 b | P x0] idx

----------------------------------------------------------------------------- *)

        simpl in *; destruct (P a) eqn:PA.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 444)
  
  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 x0 <- index_iota a.+1 b | P x0]) idx

subgoal 2 (ID 445) is:
 x < nth 0 [seq x0 <- index_iota a.+1 b | P x0] idx

----------------------------------------------------------------------------- *)

        × destruct idx; simpl; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 465)
  
  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 x0 <- index_iota a.+1 b | P x0] idx

subgoal 2 (ID 445) is:
 x < nth 0 [seq x0 <- index_iota a.+1 b | P x0] idx

----------------------------------------------------------------------------- *)

          apply IHk; try ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 468)
  
  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 x0 <- index_iota a.+1 b | P x0]

subgoal 2 (ID 445) is:
 x < nth 0 [seq x0 <- index_iota a.+1 b | P x0] idx

----------------------------------------------------------------------------- *)

            by rewrite index_iota_lt_step // //= PA //= in LT2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 445)
  
  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 x0 <- index_iota a.+1 b | P x0] idx

----------------------------------------------------------------------------- *)

        × apply IHk; try ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1419)
  
  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 x0 <- index_iota a.+1 b | P x0]

----------------------------------------------------------------------------- *)

            by rewrite index_iota_lt_step // //= PA //= in LT2.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  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 (T : eqType) (xs ys : seq T) := ∃ 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 (T : eqType) (xs ys : seq T) :=
  ∃ xs_tail, xs_tail ≠ [::] ∧ xs ++ xs_tail = ys.