Library prosa.util.bigcat


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

Welcome to Coq 8.11.2 (June 2020)

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

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

In this section, we introduce useful lemmas about the concatenation operation performed over an arbitrary range of sequences.
Section BigCatLemmas.

Consider any type supporting equality comparisons...
  Variable T: eqType.

...and a function that, given an index, yields a sequence.
  Variable f: nat → list T.

In this section, we prove that the concatenation over sequences works as expected: no element is lost during the concatenation, and no new element is introduced.
  Section BigCatElements.

First, we show that the concatenation comprises all the elements of each sequence; i.e. any element contained in one of the sequences will also be an element of the result of the concatenation.
    Lemma mem_bigcat_nat:
      ∀ x m n j,
        m ≤ j < n →
        x \in f j →
        x \in \cat_(m ≤ i < n) (f i).

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

1 subgoal (ID 37)
  
  T : eqType
  f : nat -> seq T
  ============================
  forall (x : T) (m n j : nat),
  m <= j < n -> x \in f j -> x \in \big[cat/[::]]_(m <= i < n) f i

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

    Proof.
      intros x m n j LE IN; move: LE ⇒ /andP [LE LE0].

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

1 subgoal (ID 85)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n, j : nat
  IN : x \in f j
  LE : m <= j
  LE0 : j < n
  ============================
  x \in \big[cat/[::]]_(m <= i < n) f i

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

      rewrite → big_cat_nat with (n := j); simpl; [| by ins | by apply ltnW].

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

1 subgoal (ID 90)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n, j : nat
  IN : x \in f j
  LE : m <= j
  LE0 : j < n
  ============================
  x \in \big[cat/[::]]_(m <= i < j) f i ++ \big[cat/[::]]_(j <= i < n) f i

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

      rewrite mem_cat; apply/orP; right.

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

1 subgoal (ID 129)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n, j : nat
  IN : x \in f j
  LE : m <= j
  LE0 : j < n
  ============================
  x \in \big[cat/[::]]_(j <= i < n) f i

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

      destruct n; first by rewrite ltn0 in LE0.

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

1 subgoal (ID 141)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n, j : nat
  IN : x \in f j
  LE : m <= j
  LE0 : j < n.+1
  ============================
  x \in \big[cat/[::]]_(j <= i < n.+1) f i

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

      rewrite big_nat_recl; last by ins.

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

1 subgoal (ID 190)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n, j : nat
  IN : x \in f j
  LE : m <= j
  LE0 : j < n.+1
  ============================
  x \in f j ++ \big[cat/[::]]_(j <= i < n) f i.+1

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

        by rewrite mem_cat; apply/orP; left.

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

No more subgoals.

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

    Qed.

Conversely, we prove that any element belonging to a concatenation of sequences must come from one of the sequences.
    Lemma mem_bigcat_nat_exists:
      ∀ x m n,
        x \in \cat_(m ≤ i < n) (f i) →
        ∃ i,
          x \in f i ∧ m ≤ i < n.

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

1 subgoal (ID 58)
  
  T : eqType
  f : nat -> seq T
  ============================
  forall (x : T) (m n : nat),
  x \in \big[cat/[::]]_(m <= i < n) f i ->
  exists i : nat, x \in f i /\ m <= i < n

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

    Proof.
      intros x m n IN.

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

1 subgoal (ID 62)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IN : x \in \big[cat/[::]]_(m <= i < n) f i
  ============================
  exists i : nat, x \in f i /\ m <= i < n

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

      induction n; first by rewrite big_geq // in IN.

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

1 subgoal (ID 75)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IN : x \in \big[cat/[::]]_(m <= i < n.+1) f i
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  ============================
  exists i : nat, x \in f i /\ m <= i < n.+1

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

      destruct (leqP m n); last by rewrite big_geq ?in_nil // ltnW in IN.

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

1 subgoal (ID 142)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IN : x \in \big[cat/[::]]_(m <= i < n.+1) f i
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  ============================
  exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1

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

      rewrite big_nat_recr // /= mem_cat in IN.

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

1 subgoal (ID 257)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  IN : (x \in \big[cat/[::]]_(m <= i < n) f i) || (x \in f n)
  ============================
  exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1

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

      move: IN ⇒ /orP [HEAD | TAIL].

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

2 subgoals (ID 302)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  HEAD : x \in \big[cat/[::]]_(m <= i < n) f i
  ============================
  exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1

subgoal 2 (ID 303) is:
 exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1

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

      {

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

1 subgoal (ID 302)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  HEAD : x \in \big[cat/[::]]_(m <= i < n) f i
  ============================
  exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1

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

        apply IHn in HEAD; destruct HEAD; ∃ x0.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 312)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  x0 : nat
  H : x \in f x0 /\ m <= x0 < n
  ============================
  x \in f x0 /\ m <= x0 < n.+1

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

 move: H ⇒ [H /andP [H0 H1]].

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

1 subgoal (ID 364)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  x0 : nat
  H : x \in f x0
  H0 : m <= x0
  H1 : x0 < n
  ============================
  x \in f x0 /\ m <= x0 < n.+1

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

        split; first by done.

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

1 subgoal (ID 367)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  x0 : nat
  H : x \in f x0
  H0 : m <= x0
  H1 : x0 < n
  ============================
  m <= x0 < n.+1

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

          by apply/andP; split; [by done | by apply ltnW].
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 303)

subgoal 1 (ID 303) is:
 exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1

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

}

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

1 subgoal (ID 303)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  TAIL : x \in f n
  ============================
  exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1

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

      {

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

1 subgoal (ID 303)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  TAIL : x \in f n
  ============================
  exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1

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

        ∃ n; split; first by done.

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

1 subgoal (ID 400)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IHn : x \in \big[cat/[::]]_(m <= i < n) f i ->
        exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  TAIL : x \in f n
  ============================
  m <= n < n.+1

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

        apply/andP; split; [by done | by apply ltnSn].
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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

}

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

No more subgoals.

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

    Qed.

    Lemma mem_bigcat_ord:
      ∀ x n (j: 'I_n) (f: 'I_n → list T),
        j < n →
        x \in (f j) →
        x \in \cat_(i < n) (f i).

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

1 subgoal (ID 79)
  
  T : eqType
  f : nat -> seq T
  ============================
  forall (x : T) (n : nat) (j : 'I_n) (f0 : 'I_n -> seq T),
  j < n -> x \in f0 j -> x \in \big[cat/[::]]_(i < n) f0 i

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

    Proof.
      move⇒ x; elim⇒ [//|n IHn] j f' Hj Hx.

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

1 subgoal (ID 126)
  
  T : eqType
  f : nat -> seq T
  x : T
  n : nat
  IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
        j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
  j : 'I_n.+1
  f' : 'I_n.+1 -> seq T
  Hj : j < n.+1
  Hx : x \in f' j
  ============================
  x \in \big[cat/[::]]_(i < n.+1) f' i

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

      rewrite big_ord_recr /= mem_cat; apply /orP.

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

1 focused subgoal
(shelved: 1) (ID 165)
  
  T : eqType
  f : nat -> seq T
  x : T
  n : nat
  IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
        j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
  j : 'I_n.+1
  f' : 'I_n.+1 -> seq T
  Hj : j < n.+1
  Hx : x \in f' j
  ============================
  x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i) \/
  x \in f' ord_max

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

      move: Hj; rewrite ltnS leq_eqVlt ⇒ /orP [/eqP Hj|Hj].

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

2 subgoals (ID 250)
  
  T : eqType
  f : nat -> seq T
  x : T
  n : nat
  IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
        j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
  j : 'I_n.+1
  f' : 'I_n.+1 -> seq T
  Hx : x \in f' j
  Hj : j = n
  ============================
  x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i) \/
  x \in f' ord_max

subgoal 2 (ID 251) is:
 x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i) \/
 x \in f' ord_max

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

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

1 subgoal (ID 250)
  
  T : eqType
  f : nat -> seq T
  x : T
  n : nat
  IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
        j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
  j : 'I_n.+1
  f' : 'I_n.+1 -> seq T
  Hx : x \in f' j
  Hj : j = n
  ============================
  x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i) \/
  x \in f' ord_max

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

by right; rewrite (_ : ord_max = j); [|apply ord_inj].
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 251)

subgoal 1 (ID 251) is:
 x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i) \/
 x \in f' ord_max

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

}

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

1 subgoal (ID 251)
  
  T : eqType
  f : nat -> seq T
  x : T
  n : nat
  IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
        j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
  j : 'I_n.+1
  f' : 'I_n.+1 -> seq T
  Hx : x \in f' j
  Hj : j < n
  ============================
  x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i) \/
  x \in f' ord_max

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

      left.

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

1 subgoal (ID 286)
  
  T : eqType
  f : nat -> seq T
  x : T
  n : nat
  IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
        j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
  j : 'I_n.+1
  f' : 'I_n.+1 -> seq T
  Hx : x \in f' j
  Hj : j < n
  ============================
  x \in \big[cat/[::]]_(i < n) f' (widen_ord (m:=n.+1) (leqnSn n) i)

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

      apply (IHn (Ordinal Hj)); [by []|].

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

1 subgoal (ID 290)
  
  T : eqType
  f : nat -> seq T
  x : T
  n : nat
  IHn : forall (j : 'I_n) (f : 'I_n -> seq T),
        j < n -> x \in f j -> x \in \big[cat/[::]]_(i < n) f i
  j : 'I_n.+1
  f' : 'I_n.+1 -> seq T
  Hx : x \in f' j
  Hj : j < n
  ============================
  x \in f' (widen_ord (m:=n.+1) (leqnSn n) (Ordinal (n:=n) (m:=j) Hj))

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

      by set j' := widen_ord _ _; have → : j' = j; [apply ord_inj|].

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

No more subgoals.

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

    Qed.

  End BigCatElements.

In this section, we show how we can preserve uniqueness of the elements (i.e. the absence of a duplicate) over a concatenation of sequences.
  Section BigCatDistinctElements.

Assume that there are no duplicates in each of the possible sequences to concatenate...
    Hypothesis H_uniq_seq: ∀ i, uniq (f i).

...and that there are no elements in common between the sequences.
    Hypothesis H_no_elements_in_common:
      ∀ x i1 i2, x \in f i1 → x \in f i2 → i1 = i2.

We prove that the concatenation will yield a sequence with unique elements.
    Lemma bigcat_nat_uniq:
      ∀ n1 n2,
        uniq (\cat_(n1 ≤ i < n2) (f i)).

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

1 subgoal (ID 43)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  ============================
  forall n1 n2 : nat, uniq (\big[cat/[::]]_(n1 <= i < n2) f i)

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

    Proof.
      intros n1 n2.

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

1 subgoal (ID 45)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n1, n2 : nat
  ============================
  uniq (\big[cat/[::]]_(n1 <= i < n2) f i)

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

      case (leqP n1 n2) ⇒ [LE | GT]; last by rewrite big_geq // ltnW.

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

1 subgoal (ID 48)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n1, n2 : nat
  LE : n1 <= n2
  ============================
  uniq (\big[cat/[::]]_(n1 <= i < n2) f i)

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

      rewrite -[n2](addKn n1).

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

1 subgoal (ID 94)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n1, n2 : nat
  LE : n1 <= n2
  ============================
  uniq (\big[cat/[::]]_(n1 <= i < n1 + n2 - n1) f i)

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

      rewrite -addnBA //; set delta := n2 - n1.

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

1 subgoal (ID 125)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n1, n2 : nat
  LE : n1 <= n2
  delta := n2 - n1 : nat
  ============================
  uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)

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

      induction delta; first by rewrite addn0 big_geq.

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

1 subgoal (ID 134)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n1, n2 : nat
  LE : n1 <= n2
  delta : nat
  IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
  ============================
  uniq (\big[cat/[::]]_(n1 <= i < n1 + delta.+1) f i)

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

      rewrite addnS big_nat_recr /=; last by apply leq_addr.

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

1 subgoal (ID 166)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n1, n2 : nat
  LE : n1 <= n2
  delta : nat
  IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
  ============================
  uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i ++ f (n1 + delta))

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

      rewrite cat_uniq; apply/andP; split; first by apply IHdelta.

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

1 subgoal (ID 199)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n1, n2 : nat
  LE : n1 <= n2
  delta : nat
  IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
  ============================
  ~~ has (mem (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)) (f (n1 + delta)) &&
  uniq (f (n1 + delta))

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

      apply /andP; split; last by apply H_uniq_seq.

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

1 subgoal (ID 225)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n1, n2 : nat
  LE : n1 <= n2
  delta : nat
  IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
  ============================
  ~~ has (mem (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)) (f (n1 + delta))

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

      rewrite -all_predC; apply/allP; intros x INx.

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

1 subgoal (ID 262)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n1, n2 : nat
  LE : n1 <= n2
  delta : nat
  IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
  x : T
  INx : x \in f (n1 + delta)
  ============================
  predC (mem (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)) x

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

      simpl; apply/negP; unfold not; intro BUG.

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

1 subgoal (ID 287)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n1, n2 : nat
  LE : n1 <= n2
  delta : nat
  IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
  x : T
  INx : x \in f (n1 + delta)
  BUG : x \in \big[cat/[::]]_(n1 <= i < n1 + delta) f i
  ============================
  False

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

      apply mem_bigcat_nat_exists in BUG.

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

1 subgoal (ID 288)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n1, n2 : nat
  LE : n1 <= n2
  delta : nat
  IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
  x : T
  INx : x \in f (n1 + delta)
  BUG : exists i : nat, x \in f i /\ n1 <= i < n1 + delta
  ============================
  False

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

      move: BUG ⇒ [i [IN /andP [_ LTi]]].

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

1 subgoal (ID 351)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n1, n2 : nat
  LE : n1 <= n2
  delta : nat
  IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
  x : T
  INx : x \in f (n1 + delta)
  i : nat
  IN : x \in f i
  LTi : i < n1 + delta
  ============================
  False

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

      apply H_no_elements_in_common with (i1 := i) in INx; last by done.

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

1 subgoal (ID 352)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n1, n2 : nat
  LE : n1 <= n2
  delta : nat
  IHdelta : uniq (\big[cat/[::]]_(n1 <= i < n1 + delta) f i)
  x : T
  i : nat
  INx : i = n1 + delta
  IN : x \in f i
  LTi : i < n1 + delta
  ============================
  False

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

      by rewrite INx ltnn in LTi.

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

No more subgoals.

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

    Qed.

Conversely, if the concatenation of the sequences has no duplicates, any element can only belong to a single sequence.
    Lemma bigcat_ord_uniq_reverse :
      ∀ n (f: 'I_n → list T),
        uniq (\cat_(i < n) (f i)) →
        (∀ x i1 i2,
           x \in (f i1) → x \in (f i2) → i1 = i2).

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

1 subgoal (ID 69)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  ============================
  forall (n : nat) (f0 : 'I_n -> seq T),
  uniq (\big[cat/[::]]_(i < n) f0 i) ->
  forall (x : T) (i1 i2 : 'I_n), x \in f0 i1 -> x \in f0 i2 -> i1 = i2

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

    Proof.
      case⇒ [|n]; [by move⇒ f' Huniq x; case|].

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

1 subgoal (ID 80)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  ============================
  forall f0 : 'I_n.+1 -> seq T,
  uniq (\big[cat/[::]]_(i < n.+1) f0 i) ->
  forall (x : T) (i1 i2 : 'I_n.+1), x \in f0 i1 -> x \in f0 i2 -> i1 = i2

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

      elim: n ⇒ [|n IHn] f' Huniq x i1 i2 Hi1 Hi2.

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

2 subgoals (ID 147)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_1 -> seq T
  Huniq : uniq (\big[cat/[::]]_(i < 1) f' i)
  x : T
  i1, i2 : 'I_1
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  ============================
  i1 = i2

subgoal 2 (ID 148) is:
 i1 = i2

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

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

1 subgoal (ID 147)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_1 -> seq T
  Huniq : uniq (\big[cat/[::]]_(i < 1) f' i)
  x : T
  i1, i2 : 'I_1
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  ============================
  i1 = i2

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

move: i1 i2 {Hi1 Hi2}; case; case⇒ [i1|//]; case; case⇒ [i2|//].

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

1 subgoal (ID 219)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_1 -> seq T
  Huniq : uniq (\big[cat/[::]]_(i < 1) f' i)
  x : T
  i1, i2 : 0 < 1
  ============================
  Ordinal (n:=1) (m:=0) i1 = Ordinal (n:=1) (m:=0) i2

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

        apply f_equal, eq_irrelevance.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 148)

subgoal 1 (ID 148) is:
 i1 = i2

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

}

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

1 subgoal (ID 148)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  ============================
  i1 = i2

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

      move: (leq_ord i1); rewrite leq_eqVlt ⇒ /orP [H'i1|H'i1];
        move: (leq_ord i2); rewrite leq_eqVlt ⇒ /orP [H'i2|H'i2].

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

4 subgoals (ID 347)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 == n.+1
  H'i2 : i2 == n.+1
  ============================
  i1 = i2

subgoal 2 (ID 348) is:
 i1 = i2
subgoal 3 (ID 395) is:
 i1 = i2
subgoal 4 (ID 396) is:
 i1 = i2

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

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

1 subgoal (ID 347)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 == n.+1
  H'i2 : i2 == n.+1
  ============================
  i1 = i2

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

by apply ord_inj; move: H'i1 H'i2 ⇒ /eqP → /eqP →.
(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 348)

subgoal 1 (ID 348) is:
 i1 = i2
subgoal 2 (ID 395) is:
 i1 = i2
subgoal 3 (ID 396) is:
 i1 = i2

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

}

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

3 subgoals (ID 348)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 == n.+1
  H'i2 : i2 < n.+1
  ============================
  i1 = i2

subgoal 2 (ID 395) is:
 i1 = i2
subgoal 3 (ID 396) is:
 i1 = i2

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

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

1 subgoal (ID 348)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 == n.+1
  H'i2 : i2 < n.+1
  ============================
  i1 = i2

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

exfalso.

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

1 subgoal (ID 475)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 == n.+1
  H'i2 : i2 < n.+1
  ============================
  False

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

        move: Huniq; rewrite big_ord_recr cat_uniq ⇒ /andP [_ /andP [H _]].

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

1 subgoal (ID 569)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 == n.+1
  H'i2 : i2 < n.+1
  H : ~~
      has
        (mem
           (\big[cat_monoid T/[::]]_(i < n.+1) f'
                                                 (widen_ord (m:=n.+2)
                                                 (leqnSn n.+1) i)))
        (f' ord_max)
  ============================
  False

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

        move: H; apply /negP; rewrite Bool.negb_involutive.

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

1 subgoal (ID 616)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 == n.+1
  H'i2 : i2 < n.+1
  ============================
  has
    (mem
       (\big[cat_monoid T/[::]]_(i < n.+1) f'
                                             (widen_ord (m:=n.+2)
                                                (leqnSn n.+1) i)))
    (f' ord_max)

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

        apply /hasP; ∃ x ⇒ /=.

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

2 subgoals (ID 648)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 == n.+1
  H'i2 : i2 < n.+1
  ============================
  x \in f' ord_max

subgoal 2 (ID 649) is:
 x \in \big[cat/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)

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

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

1 subgoal (ID 648)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 == n.+1
  H'i2 : i2 < n.+1
  ============================
  x \in f' ord_max

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

set o := ord_max; suff → : o = i1; [by []|].

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

1 subgoal (ID 656)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 == n.+1
  H'i2 : i2 < n.+1
  o := ord_max : 'I_n.+2
  ============================
  o = i1

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

          by apply ord_inj; move: H'i1 ⇒ /eqP →.
(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 649)

subgoal 1 (ID 649) is:
 x \in \big[cat/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
subgoal 2 (ID 395) is:
 i1 = i2
subgoal 3 (ID 396) is:
 i1 = i2

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

}

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

1 subgoal (ID 649)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 == n.+1
  H'i2 : i2 < n.+1
  ============================
  x \in \big[cat/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)

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

        apply (mem_bigcat_ord _ _ (Ordinal H'i2)) ⇒ //.

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

1 subgoal (ID 708)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 == n.+1
  H'i2 : i2 < n.+1
  ============================
  x
    \in f'
          (widen_ord (m:=n.+2) (leqnSn n.+1) (Ordinal (n:=n.+1) (m:=i2) H'i2))

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

        by set o := widen_ord _ _; suff → : o = i2; [|apply ord_inj].
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 395)

subgoal 1 (ID 395) is:
 i1 = i2
subgoal 2 (ID 396) is:
 i1 = i2

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

}

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

2 subgoals (ID 395)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 < n.+1
  H'i2 : i2 == n.+1
  ============================
  i1 = i2

subgoal 2 (ID 396) is:
 i1 = i2

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

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

1 subgoal (ID 395)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 < n.+1
  H'i2 : i2 == n.+1
  ============================
  i1 = i2

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

exfalso.

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

1 subgoal (ID 748)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 < n.+1
  H'i2 : i2 == n.+1
  ============================
  False

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

        move: Huniq; rewrite big_ord_recr cat_uniq ⇒ /andP [_ /andP [H _]].

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

1 subgoal (ID 842)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 < n.+1
  H'i2 : i2 == n.+1
  H : ~~
      has
        (mem
           (\big[cat_monoid T/[::]]_(i < n.+1) f'
                                                 (widen_ord (m:=n.+2)
                                                 (leqnSn n.+1) i)))
        (f' ord_max)
  ============================
  False

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

        move: H; apply /negP; rewrite Bool.negb_involutive.

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

1 subgoal (ID 889)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 < n.+1
  H'i2 : i2 == n.+1
  ============================
  has
    (mem
       (\big[cat_monoid T/[::]]_(i < n.+1) f'
                                             (widen_ord (m:=n.+2)
                                                (leqnSn n.+1) i)))
    (f' ord_max)

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

        apply /hasP; ∃ x ⇒ /=.

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

2 subgoals (ID 921)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 < n.+1
  H'i2 : i2 == n.+1
  ============================
  x \in f' ord_max

subgoal 2 (ID 922) is:
 x \in \big[cat/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)

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

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

1 subgoal (ID 921)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 < n.+1
  H'i2 : i2 == n.+1
  ============================
  x \in f' ord_max

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

set o := ord_max; suff → : o = i2; [by []|].

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

1 subgoal (ID 929)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 < n.+1
  H'i2 : i2 == n.+1
  o := ord_max : 'I_n.+2
  ============================
  o = i2

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

          by apply ord_inj; move: H'i2 ⇒ /eqP →.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 922)

subgoal 1 (ID 922) is:
 x \in \big[cat/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
subgoal 2 (ID 396) is:
 i1 = i2

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

}

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

1 subgoal (ID 922)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 < n.+1
  H'i2 : i2 == n.+1
  ============================
  x \in \big[cat/[::]]_(i < n.+1) f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)

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

        apply (mem_bigcat_ord _ _ (Ordinal H'i1)) ⇒ //.

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

1 subgoal (ID 981)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 < n.+1
  H'i2 : i2 == n.+1
  ============================
  x
    \in f'
          (widen_ord (m:=n.+2) (leqnSn n.+1) (Ordinal (n:=n.+1) (m:=i1) H'i1))

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

        by set o := widen_ord _ _; suff → : o = i1; [|apply ord_inj].
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 396)

subgoal 1 (ID 396) is:
 i1 = i2

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

}

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

1 subgoal (ID 396)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  Huniq : uniq (\big[cat/[::]]_(i < n.+2) f' i)
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 < n.+1
  H'i2 : i2 < n.+1
  ============================
  i1 = i2

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

      move: Huniq; rewrite big_ord_recr cat_uniq ⇒ /andP [Huniq _].

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

1 subgoal (ID 1076)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 < n.+1
  H'i2 : i2 < n.+1
  Huniq : uniq
            (\big[cat_monoid T/[::]]_(i < n.+1) f'
                                                 (widen_ord (m:=n.+2)
                                                 (leqnSn n.+1) i))
  ============================
  i1 = i2

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

      apply ord_inj; rewrite -(inordK H'i1) -(inordK H'i2); apply f_equal.

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

1 subgoal (ID 1090)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 < n.+1
  H'i2 : i2 < n.+1
  Huniq : uniq
            (\big[cat_monoid T/[::]]_(i < n.+1) f'
                                                 (widen_ord (m:=n.+2)
                                                 (leqnSn n.+1) i))
  ============================
  inord i1 = inord i2

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

      apply (IHn _ Huniq x).

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

2 subgoals (ID 1093)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 < n.+1
  H'i2 : i2 < n.+1
  Huniq : uniq
            (\big[cat_monoid T/[::]]_(i < n.+1) f'
                                                 (widen_ord (m:=n.+2)
                                                 (leqnSn n.+1) i))
  ============================
  x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i1))

subgoal 2 (ID 1094) is:
 x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i2))

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

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

1 subgoal (ID 1093)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 < n.+1
  H'i2 : i2 < n.+1
  Huniq : uniq
            (\big[cat_monoid T/[::]]_(i < n.+1) f'
                                                 (widen_ord (m:=n.+2)
                                                 (leqnSn n.+1) i))
  ============================
  x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i1))

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

set i1' := widen_ord _ _; suff → : i1' = i1; [by []|].

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

1 subgoal (ID 1106)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 < n.+1
  H'i2 : i2 < n.+1
  Huniq : uniq
            (\big[cat_monoid T/[::]]_(i < n.+1) f'
                                                 (widen_ord (m:=n.+2)
                                                 (leqnSn n.+1) i))
  i1' := widen_ord (m:=n.+2) (leqnSn n.+1) (inord i1) : 'I_n.+2
  ============================
  i1' = i1

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

        by apply ord_inj; rewrite /= inordK.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1094)

subgoal 1 (ID 1094) is:
 x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i2))

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

}

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

1 subgoal (ID 1094)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 < n.+1
  H'i2 : i2 < n.+1
  Huniq : uniq
            (\big[cat_monoid T/[::]]_(i < n.+1) f'
                                                 (widen_ord (m:=n.+2)
                                                 (leqnSn n.+1) i))
  ============================
  x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i2))

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

      set i2' := widen_ord _ _; suff → : i2' = i2; [by []|].

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

1 subgoal (ID 1130)
  
  T : eqType
  f : nat -> seq T
  H_uniq_seq : forall i : nat, uniq (f i)
  H_no_elements_in_common : forall (x : T) (i1 i2 : nat),
                            x \in f i1 -> x \in f i2 -> i1 = i2
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\big[cat/[::]]_(i < n.+1) f i) ->
        forall (x : T) (i1 i2 : 'I_n.+1), x \in f i1 -> x \in f i2 -> i1 = i2
  f' : 'I_n.+2 -> seq T
  x : T
  i1, i2 : 'I_n.+2
  Hi1 : x \in f' i1
  Hi2 : x \in f' i2
  H'i1 : i1 < n.+1
  H'i2 : i2 < n.+1
  Huniq : uniq
            (\big[cat_monoid T/[::]]_(i < n.+1) f'
                                                 (widen_ord (m:=n.+2)
                                                 (leqnSn n.+1) i))
  i2' := widen_ord (m:=n.+2) (leqnSn n.+1) (inord i2) : 'I_n.+2
  ============================
  i2' = i2

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

      by apply ord_inj; rewrite /= inordK.

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

No more subgoals.

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

    Qed.

  End BigCatDistinctElements.

We show that filtering a concatenated sequence by any predicate [P] is the same as concatenating the elements of the sequence that satisfy [P].
  Lemma cat_filter_eq_filter_cat:
    ∀ {X : Type} (F : nat → seq X) (P : X → bool) (t1 t2 : nat),
      [seq x <- \cat_(t1≤t<t2) F t | P x] = \cat_(t1≤t<t2)[seq x <- F t | P x].

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

1 subgoal (ID 36)
  
  T : eqType
  f : nat -> seq T
  ============================
  forall (X : Type) (F : nat -> seq X) (P : X -> bool) (t1 t2 : nat),
  [seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
  \big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]

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

  Proof.
    intros.

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

1 subgoal (ID 41)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  P : X -> bool
  t1, t2 : nat
  ============================
  [seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
  \big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]

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

    specialize (leq_total t1 t2) ⇒ /orP [T1_LT | T2_LT].

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

2 subgoals (ID 86)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  P : X -> bool
  t1, t2 : nat
  T1_LT : t1 <= t2
  ============================
  [seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
  \big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]

subgoal 2 (ID 87) is:
 [seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
 \big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]

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

    + have EX: ∃ Δ, t2 = t1 + Δ by ∃ (t2 - t1); ssrlia.

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

2 subgoals (ID 235)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  P : X -> bool
  t1, t2 : nat
  T1_LT : t1 <= t2
  EX : exists Δ : nat, t2 = t1 + Δ
  ============================
  [seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
  \big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]

subgoal 2 (ID 87) is:
 [seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
 \big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]

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

      move: EX ⇒ [Δ EQ]; subst t2.

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

2 subgoals (ID 254)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  P : X -> bool
  t1, Δ : nat
  T1_LT : t1 <= t1 + Δ
  ============================
  [seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ) F t | P x] =
  \big[cat/[::]]_(t1 <= t < t1 + Δ) [seq x <- F t | P x]

subgoal 2 (ID 87) is:
 [seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
 \big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]

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

      induction Δ.

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

3 subgoals (ID 263)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  P : X -> bool
  t1 : nat
  T1_LT : t1 <= t1 + 0
  ============================
  [seq x <- \big[cat/[::]]_(t1 <= t < t1 + 0) F t | P x] =
  \big[cat/[::]]_(t1 <= t < t1 + 0) [seq x <- F t | P x]

subgoal 2 (ID 267) is:
 [seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t | P x] =
 \big[cat/[::]]_(t1 <= t < t1 + Δ.+1) [seq x <- F t | P x]
subgoal 3 (ID 87) is:
 [seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
 \big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]

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

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

1 subgoal (ID 263)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  P : X -> bool
  t1 : nat
  T1_LT : t1 <= t1 + 0
  ============================
  [seq x <- \big[cat/[::]]_(t1 <= t < t1 + 0) F t | P x] =
  \big[cat/[::]]_(t1 <= t < t1 + 0) [seq x <- F t | P x]

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

now rewrite addn0 !big_geq ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 267)

subgoal 1 (ID 267) is:
 [seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t | P x] =
 \big[cat/[::]]_(t1 <= t < t1 + Δ.+1) [seq x <- F t | P x]
subgoal 2 (ID 87) is:
 [seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
 \big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]

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

}

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

2 subgoals (ID 267)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  P : X -> bool
  t1, Δ : nat
  T1_LT : t1 <= t1 + Δ.+1
  IHΔ : t1 <= t1 + Δ ->
        [seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ) F t | P x] =
        \big[cat/[::]]_(t1 <= t < t1 + Δ) [seq x <- F t | P x]
  ============================
  [seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t | P x] =
  \big[cat/[::]]_(t1 <= t < t1 + Δ.+1) [seq x <- F t | P x]

subgoal 2 (ID 87) is:
 [seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
 \big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]

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

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

1 subgoal (ID 267)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  P : X -> bool
  t1, Δ : nat
  T1_LT : t1 <= t1 + Δ.+1
  IHΔ : t1 <= t1 + Δ ->
        [seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ) F t | P x] =
        \big[cat/[::]]_(t1 <= t < t1 + Δ) [seq x <- F t | P x]
  ============================
  [seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t | P x] =
  \big[cat/[::]]_(t1 <= t < t1 + Δ.+1) [seq x <- F t | P x]

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

rewrite addnS !big_nat_recr ⇒ //=; try by rewrite leq_addr.

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

1 subgoal (ID 366)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  P : X -> bool
  t1, Δ : nat
  T1_LT : t1 <= t1 + Δ.+1
  IHΔ : t1 <= t1 + Δ ->
        [seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ) F t | P x] =
        \big[cat/[::]]_(t1 <= t < t1 + Δ) [seq x <- F t | P x]
  ============================
  [seq x <- \big[cat/[::]]_(t1 <= i < t1 + Δ) F i ++ F (t1 + Δ) | P x] =
  \big[cat/[::]]_(t1 <= i < t1 + Δ) [seq x <- F i | P x] ++
  [seq x <- F (t1 + Δ) | P x]

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

        rewrite filter_cat IHΔ ⇒ //.

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

1 subgoal (ID 454)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  P : X -> bool
  t1, Δ : nat
  T1_LT : t1 <= t1 + Δ.+1
  IHΔ : t1 <= t1 + Δ ->
        [seq x <- \big[cat/[::]]_(t1 <= t < t1 + Δ) F t | P x] =
        \big[cat/[::]]_(t1 <= t < t1 + Δ) [seq x <- F t | P x]
  ============================
  t1 <= t1 + Δ

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

        now ssrlia.

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

1 subgoal (ID 87)

subgoal 1 (ID 87) is:
 [seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
 \big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]

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

      }

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

1 subgoal (ID 87)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  P : X -> bool
  t1, t2 : nat
  T2_LT : t2 <= t1
  ============================
  [seq x <- \big[cat/[::]]_(t1 <= t < t2) F t | P x] =
  \big[cat/[::]]_(t1 <= t < t2) [seq x <- F t | P x]

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

    + now rewrite !big_geq ⇒ //.

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

No more subgoals.

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

  Qed.

We show that the size of a concatenated sequence is the same as summation of sizes of each element of the sequence.
  Lemma size_big_nat:
    ∀ {X : Type} (F : nat → seq X) (t1 t2 : nat),
      \sum_(t1 ≤ t < t2) size (F t) =
      size (\cat_(t1 ≤ t < t2) F t).

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

1 subgoal (ID 51)
  
  T : eqType
  f : nat -> seq T
  ============================
  forall (X : Type) (F : nat -> seq X) (t1 t2 : nat),
  \sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)

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

  Proof.
    intros.

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

1 subgoal (ID 55)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  t1, t2 : nat
  ============================
  \sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)

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

    specialize (leq_total t1 t2) ⇒ /orP [T1_LT | T2_LT].

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

2 subgoals (ID 100)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  t1, t2 : nat
  T1_LT : t1 <= t2
  ============================
  \sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)

subgoal 2 (ID 101) is:
 \sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)

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

    + have EX: ∃ Δ, t2 = t1 + Δ by ∃ (t2 - t1); ssrlia.

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

2 subgoals (ID 249)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  t1, t2 : nat
  T1_LT : t1 <= t2
  EX : exists Δ : nat, t2 = t1 + Δ
  ============================
  \sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)

subgoal 2 (ID 101) is:
 \sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)

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

      move: EX ⇒ [Δ EQ]; subst t2.

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

2 subgoals (ID 268)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  t1, Δ : nat
  T1_LT : t1 <= t1 + Δ
  ============================
  \sum_(t1 <= t < t1 + Δ) size (F t) =
  size (\big[cat/[::]]_(t1 <= t < t1 + Δ) F t)

subgoal 2 (ID 101) is:
 \sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)

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

      induction Δ.

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

3 subgoals (ID 277)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  t1 : nat
  T1_LT : t1 <= t1 + 0
  ============================
  \sum_(t1 <= t < t1 + 0) size (F t) =
  size (\big[cat/[::]]_(t1 <= t < t1 + 0) F t)

subgoal 2 (ID 281) is:
 \sum_(t1 <= t < t1 + Δ.+1) size (F t) =
 size (\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t)
subgoal 3 (ID 101) is:
 \sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)

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

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

1 subgoal (ID 277)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  t1 : nat
  T1_LT : t1 <= t1 + 0
  ============================
  \sum_(t1 <= t < t1 + 0) size (F t) =
  size (\big[cat/[::]]_(t1 <= t < t1 + 0) F t)

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

now rewrite addn0 !big_geq ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 281)

subgoal 1 (ID 281) is:
 \sum_(t1 <= t < t1 + Δ.+1) size (F t) =
 size (\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t)
subgoal 2 (ID 101) is:
 \sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)

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

}

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

2 subgoals (ID 281)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  t1, Δ : nat
  T1_LT : t1 <= t1 + Δ.+1
  IHΔ : t1 <= t1 + Δ ->
        \sum_(t1 <= t < t1 + Δ) size (F t) =
        size (\big[cat/[::]]_(t1 <= t < t1 + Δ) F t)
  ============================
  \sum_(t1 <= t < t1 + Δ.+1) size (F t) =
  size (\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t)

subgoal 2 (ID 101) is:
 \sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)

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

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

1 subgoal (ID 281)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  t1, Δ : nat
  T1_LT : t1 <= t1 + Δ.+1
  IHΔ : t1 <= t1 + Δ ->
        \sum_(t1 <= t < t1 + Δ) size (F t) =
        size (\big[cat/[::]]_(t1 <= t < t1 + Δ) F t)
  ============================
  \sum_(t1 <= t < t1 + Δ.+1) size (F t) =
  size (\big[cat/[::]]_(t1 <= t < t1 + Δ.+1) F t)

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

rewrite addnS !big_nat_recr ⇒ //=; try by rewrite leq_addr.

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

1 subgoal (ID 379)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  t1, Δ : nat
  T1_LT : t1 <= t1 + Δ.+1
  IHΔ : t1 <= t1 + Δ ->
        \sum_(t1 <= t < t1 + Δ) size (F t) =
        size (\big[cat/[::]]_(t1 <= t < t1 + Δ) F t)
  ============================
  \sum_(t1 <= i < t1 + Δ) size (F i) + size (F (t1 + Δ)) =
  size (\big[cat/[::]]_(t1 <= i < t1 + Δ) F i ++ F (t1 + Δ))

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

        rewrite size_cat IHΔ ⇒ //.

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

1 subgoal (ID 466)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  t1, Δ : nat
  T1_LT : t1 <= t1 + Δ.+1
  IHΔ : t1 <= t1 + Δ ->
        \sum_(t1 <= t < t1 + Δ) size (F t) =
        size (\big[cat/[::]]_(t1 <= t < t1 + Δ) F t)
  ============================
  t1 <= t1 + Δ

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

        now ssrlia.

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

1 subgoal (ID 101)

subgoal 1 (ID 101) is:
 \sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)

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

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

1 subgoal (ID 101)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  t1, t2 : nat
  T2_LT : t2 <= t1
  ============================
  \sum_(t1 <= t < t2) size (F t) = size (\big[cat/[::]]_(t1 <= t < t2) F t)

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

        
    + now rewrite !big_geq ⇒ //.

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

No more subgoals.

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

  Qed.

End BigCatLemmas.