Library prosa.util.bigcat


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

Welcome to Coq 8.13.0 (January 2021)

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

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 prosa.util.list.

In this section, we introduce useful lemmas about the concatenation operation performed over arbitrary sequences.
Section BigCatNatLemmas.

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

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 35)
  
  T : eqType
  f : nat -> seq T
  ============================
  forall (x : T) (m n j : nat),
  m <= j < n -> x \in f j -> x \in \cat_(m<=i<n)f i

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

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

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

1 subgoal (ID 82)
  
  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 \cat_(m<=i<n)f i

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

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

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

1 subgoal (ID 86)
  
  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 \cat_(m<=i<j)f i ++ \cat_(j<=i<n)f i

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

      rewrite mem_cat; apply/orP; right.

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

1 subgoal (ID 123)
  
  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 \cat_(j<=i<n)f i

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

      destruct n; first by rewrite ltn0 in LE0.

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

1 subgoal (ID 135)
  
  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 \cat_(j<=i<n.+1)f i

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

      rewrite big_nat_recl; last by ins.

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

1 subgoal (ID 183)
  
  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 ++ \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 56)
  
  T : eqType
  f : nat -> seq T
  ============================
  forall (x : T) (m n : nat),
  x \in \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 60)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IN : x \in \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 73)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IN : x \in \cat_(m<=i<n.+1)f i
  IHn : x \in \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 171)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IN : x \in \cat_(m<=i<n.+1)f i
  IHn : x \in \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 284)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IHn : x \in \cat_(m<=i<n)f i -> exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  IN : (x \in \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 328)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IHn : x \in \cat_(m<=i<n)f i -> exists i : nat, x \in f i /\ m <= i < n
  i : m <= n
  HEAD : x \in \cat_(m<=i<n)f i
  ============================
  exists i0 : nat, x \in f i0 /\ m <= i0 < n.+1

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

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

      - apply IHn in HEAD; destruct HEAD; ∃ x0.

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

2 subgoals (ID 338)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IHn : x \in \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

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

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

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

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

2 subgoals (ID 389)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IHn : x \in \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

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

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

        split; first by done.

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

2 subgoals (ID 392)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IHn : x \in \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

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

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

        by apply/andP; split; last by apply ltnW.

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

1 subgoal (ID 329)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IHn : x \in \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 425)
  
  T : eqType
  f : nat -> seq T
  x : T
  m, n : nat
  IHn : x \in \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

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

        by apply/andP; split; last apply ltnSn.

(* ----------------------------------[ 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 77)
  
  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 \cat_(i<n)f0 i

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

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

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

1 subgoal (ID 123)
  
  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 \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 \cat_(i<n.+1)f' i

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

      rewrite big_ord_recr /= mem_cat; apply /orP.

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

1 focused subgoal
(shelved: 1) (ID 162)
  
  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 \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 \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 245)
  
  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 \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 \cat_(i<n)f' (widen_ord (m:=n.+1) (leqnSn n) i) \/ x \in f' ord_max

subgoal 2 (ID 246) is:
 x \in \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 246)
  
  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 \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 \cat_(i<n)f' (widen_ord (m:=n.+1) (leqnSn n) i) \/ x \in f' ord_max

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

      - left.

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

1 subgoal (ID 278)
  
  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 \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 \cat_(i<n)f' (widen_ord (m:=n.+1) (leqnSn n) i)

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

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

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

1 subgoal (ID 282)
  
  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 \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 BigCatNatElements.

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

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 40)
  
  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 (\cat_(n1<=i<n2)f i)

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

    Proof.
      intros n1 n2.

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

1 subgoal (ID 42)
  
  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 (\cat_(n1<=i<n2)f i)

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

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

(* ----------------------------------[ 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
  LE : n1 <= n2
  ============================
  uniq (\cat_(n1<=i<n2)f i)

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

      rewrite -[n2](addKn n1).

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

1 subgoal (ID 90)
  
  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 (\cat_(n1<=i<n1 + n2 - n1)f i)

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

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

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

1 subgoal (ID 120)
  
  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 (\cat_(n1<=i<n1 + delta)f i)

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

      induction delta; first by rewrite addn0 big_geq.

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

1 subgoal (ID 129)
  
  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 (\cat_(n1<=i<n1 + delta)f i)
  ============================
  uniq (\cat_(n1<=i<n1 + delta.+1)f i)

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

      rewrite addnS big_nat_recr /=; last by apply leq_addr.

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

1 subgoal (ID 161)
  
  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 (\cat_(n1<=i<n1 + delta)f i)
  ============================
  uniq (\cat_(n1<=i<n1 + delta)f i ++ f (n1 + delta))

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

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

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

1 subgoal (ID 194)
  
  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 (\cat_(n1<=i<n1 + delta)f i)
  ============================
  ~~ has (mem (\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 220)
  
  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 (\cat_(n1<=i<n1 + delta)f i)
  ============================
  ~~ has (mem (\cat_(n1<=i<n1 + delta)f i)) (f (n1 + delta))

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

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

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

1 subgoal (ID 257)
  
  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 (\cat_(n1<=i<n1 + delta)f i)
  x : T
  INx : x \in f (n1 + delta)
  ============================
  predC (mem (\cat_(n1<=i<n1 + delta)f i)) x

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

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

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

1 subgoal (ID 280)
  
  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 (\cat_(n1<=i<n1 + delta)f i)
  x : T
  INx : x \in f (n1 + delta)
  BUG : x \in \cat_(n1<=i<n1 + delta)f i
  ============================
  False

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

      apply mem_bigcat_nat_exists in BUG.

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

1 subgoal (ID 282)
  
  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 (\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 343)
  
  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 (\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 345)
  
  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 (\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 65)
  
  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 (\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 76)
  
  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 (\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 142)
  
  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 (\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 143) is:
 i1 = i2

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

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

1 subgoal (ID 142)
  
  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 (\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 213)
  
  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 (\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

subgoal 1 (ID 143) is:
 i1 = i2

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

}

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

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

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

2 subgoals (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
  n : nat
  IHn : forall f : 'I_n.+1 -> seq T,
        uniq (\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 (\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
  ============================
  i1 = i2

subgoal 2 (ID 288) is:
 i1 = i2

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

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

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

4 subgoals (ID 338)
  
  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 (\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 (\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 339) is:
 i1 = i2
subgoal 3 (ID 385) is:
 i1 = i2
subgoal 4 (ID 386) is:
 i1 = i2

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

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

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

subgoal 1 (ID 339) is:
 i1 = i2
subgoal 2 (ID 385) is:
 i1 = i2
subgoal 3 (ID 386) is:
 i1 = i2

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

}

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

3 subgoals (ID 339)
  
  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 (\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 (\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 385) is:
 i1 = i2
subgoal 3 (ID 386) is:
 i1 = i2

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

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

1 subgoal (ID 339)
  
  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 (\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 (\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 463)
  
  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 (\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 (\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 555)
  
  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 (\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 602)
  
  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 (\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 634)
  
  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 (\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 635) is:
 x \in \cat_(i<n.+1)f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)

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

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

1 subgoal (ID 634)
  
  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 (\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 641)
  
  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 (\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

subgoal 1 (ID 635) is:
 x \in \cat_(i<n.+1)f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
subgoal 2 (ID 385) is:
 i1 = i2
subgoal 3 (ID 386) is:
 i1 = i2

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

}

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

1 subgoal (ID 635)
  
  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 (\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 \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 692)
  
  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 (\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

subgoal 1 (ID 385) is:
 i1 = i2
subgoal 2 (ID 386) is:
 i1 = i2

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

}

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

2 subgoals (ID 385)
  
  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 (\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 (\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 386) is:
 i1 = i2

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

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

1 subgoal (ID 385)
  
  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 (\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 (\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 730)
  
  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 (\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 (\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 822)
  
  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 (\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 869)
  
  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 (\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 901)
  
  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 (\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 902) is:
 x \in \cat_(i<n.+1)f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)

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

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

1 subgoal (ID 901)
  
  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 (\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 908)
  
  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 (\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

subgoal 1 (ID 902) is:
 x \in \cat_(i<n.+1)f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)
subgoal 2 (ID 386) is:
 i1 = i2

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

}

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

1 subgoal (ID 902)
  
  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 (\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 \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 959)
  
  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 (\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

subgoal 1 (ID 386) is:
 i1 = i2

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

}

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

1 subgoal (ID 386)
  
  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 (\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 (\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 1051)
  
  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 (\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 1065)
  
  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 (\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 1068)
  
  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 (\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 1069) is:
 x \in f' (widen_ord (m:=n.+2) (leqnSn n.+1) (inord i2))

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

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

1 subgoal (ID 1068)
  
  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 (\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 1080)
  
  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 (\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

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

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

}

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

1 subgoal (ID 1069)
  
  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 (\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 1103)
  
  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 (\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 BigCatNatDistinctElements.

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 bigcat_nat_filter_eq_filter_bigcat_nat:
    ∀ {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 33)
  
  T : eqType
  f : nat -> seq T
  ============================
  forall (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]

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

  Proof.
    intros.

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

1 subgoal (ID 38)
  
  T : eqType
  f : nat -> seq T
  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]

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

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

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

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

subgoal 2 (ID 83) is:
 [seq x <- \cat_(t1<=t<t2)F t | P x] = \cat_(t1<=t<t2)[seq x <- F t | P x]

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

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

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

2 subgoals (ID 190)
  
  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 <- \cat_(t1<=t<t2)F t | P x] = \cat_(t1<=t<t2)[seq x <- F t | P x]

subgoal 2 (ID 83) is:
 [seq x <- \cat_(t1<=t<t2)F t | P x] = \cat_(t1<=t<t2)[seq x <- F t | P x]

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

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

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

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

subgoal 2 (ID 83) is:
 [seq x <- \cat_(t1<=t<t2)F t | P x] = \cat_(t1<=t<t2)[seq x <- F t | P x]

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

      induction Δ.

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

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

subgoal 2 (ID 222) is:
 [seq x <- \cat_(t1<=t<t1 + Δ.+1)F t | P x] =
 \cat_(t1<=t<t1 + Δ.+1)[seq x <- F t | P x]
subgoal 3 (ID 83) is:
 [seq x <- \cat_(t1<=t<t2)F t | P x] = \cat_(t1<=t<t2)[seq x <- F t | P x]

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

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

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

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

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

2 subgoals

subgoal 1 (ID 222) is:
 [seq x <- \cat_(t1<=t<t1 + Δ.+1)F t | P x] =
 \cat_(t1<=t<t1 + Δ.+1)[seq x <- F t | P x]
subgoal 2 (ID 83) is:
 [seq x <- \cat_(t1<=t<t2)F t | P x] = \cat_(t1<=t<t2)[seq x <- F t | P x]

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

}

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

2 subgoals (ID 222)
  
  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 <- \cat_(t1<=t<t1 + Δ)F t | P x] =
        \cat_(t1<=t<t1 + Δ)[seq x <- F t | P x]
  ============================
  [seq x <- \cat_(t1<=t<t1 + Δ.+1)F t | P x] =
  \cat_(t1<=t<t1 + Δ.+1)[seq x <- F t | P x]

subgoal 2 (ID 83) is:
 [seq x <- \cat_(t1<=t<t2)F t | P x] = \cat_(t1<=t<t2)[seq x <- F t | P x]

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

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

1 subgoal (ID 222)
  
  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 <- \cat_(t1<=t<t1 + Δ)F t | P x] =
        \cat_(t1<=t<t1 + Δ)[seq x <- F t | P x]
  ============================
  [seq x <- \cat_(t1<=t<t1 + Δ.+1)F t | P x] =
  \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 321)
  
  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 <- \cat_(t1<=t<t1 + Δ)F t | P x] =
        \cat_(t1<=t<t1 + Δ)[seq x <- F t | P x]
  ============================
  [seq x <- \cat_(t1<=i<t1 + Δ)F i ++ F (t1 + Δ) | P x] =
  \cat_(t1<=i<t1 + Δ)[seq x <- F i | P x] ++ [seq x <- F (t1 + Δ) | P x]

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

        rewrite filter_cat IHΔ ⇒ //.

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

1 subgoal (ID 406)
  
  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 <- \cat_(t1<=t<t1 + Δ)F t | P x] =
        \cat_(t1<=t<t1 + Δ)[seq x <- F t | P x]
  ============================
  t1 <= t1 + Δ

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

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

1 subgoal

subgoal 1 (ID 83) is:
 [seq x <- \cat_(t1<=t<t2)F t | P x] = \cat_(t1<=t<t2)[seq x <- F t | P x]

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

}

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

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

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

    + by 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 47)
  
  T : eqType
  f : nat -> seq T
  ============================
  forall (X : Type) (F : nat -> seq X) (t1 t2 : nat),
  \sum_(t1 <= t < t2) size (F t) = size (\cat_(t1<=t<t2)F t)

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

  Proof.
    intros.

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

1 subgoal (ID 51)
  
  T : eqType
  f : nat -> seq T
  X : Type
  F : nat -> seq X
  t1, t2 : nat
  ============================
  \sum_(t1 <= t < t2) size (F t) = size (\cat_(t1<=t<t2)F t)

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

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

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

2 subgoals (ID 95)
  
  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 (\cat_(t1<=t<t2)F t)

subgoal 2 (ID 96) is:
 \sum_(t1 <= t < t2) size (F t) = size (\cat_(t1<=t<t2)F t)

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

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

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

2 subgoals (ID 203)
  
  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 (\cat_(t1<=t<t2)F t)

subgoal 2 (ID 96) is:
 \sum_(t1 <= t < t2) size (F t) = size (\cat_(t1<=t<t2)F t)

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

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

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

2 subgoals (ID 222)
  
  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 (\cat_(t1<=t<t1 + Δ)F t)

subgoal 2 (ID 96) is:
 \sum_(t1 <= t < t2) size (F t) = size (\cat_(t1<=t<t2)F t)

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

      induction Δ.

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

3 subgoals (ID 231)
  
  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 (\cat_(t1<=t<t1 + 0)F t)

subgoal 2 (ID 235) is:
 \sum_(t1 <= t < t1 + Δ.+1) size (F t) = size (\cat_(t1<=t<t1 + Δ.+1)F t)
subgoal 3 (ID 96) is:
 \sum_(t1 <= t < t2) size (F t) = size (\cat_(t1<=t<t2)F t)

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

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

1 subgoal (ID 231)
  
  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 (\cat_(t1<=t<t1 + 0)F t)

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

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

2 subgoals

subgoal 1 (ID 235) is:
 \sum_(t1 <= t < t1 + Δ.+1) size (F t) = size (\cat_(t1<=t<t1 + Δ.+1)F t)
subgoal 2 (ID 96) is:
 \sum_(t1 <= t < t2) size (F t) = size (\cat_(t1<=t<t2)F t)

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

}

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

2 subgoals (ID 235)
  
  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 (\cat_(t1<=t<t1 + Δ)F t)
  ============================
  \sum_(t1 <= t < t1 + Δ.+1) size (F t) = size (\cat_(t1<=t<t1 + Δ.+1)F t)

subgoal 2 (ID 96) is:
 \sum_(t1 <= t < t2) size (F t) = size (\cat_(t1<=t<t2)F t)

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

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

1 subgoal (ID 235)
  
  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 (\cat_(t1<=t<t1 + Δ)F t)
  ============================
  \sum_(t1 <= t < t1 + Δ.+1) size (F t) = size (\cat_(t1<=t<t1 + Δ.+1)F t)

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

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

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

1 subgoal (ID 333)
  
  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 (\cat_(t1<=t<t1 + Δ)F t)
  ============================
  \sum_(t1 <= i < t1 + Δ) size (F i) + size (F (t1 + Δ)) =
  size (\cat_(t1<=i<t1 + Δ)F i ++ F (t1 + Δ))

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

        rewrite size_cat IHΔ ⇒ //.

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

1 subgoal (ID 417)
  
  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 (\cat_(t1<=t<t1 + Δ)F t)
  ============================
  t1 <= t1 + Δ

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

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

1 subgoal

subgoal 1 (ID 96) is:
 \sum_(t1 <= t < t2) size (F t) = size (\cat_(t1<=t<t2)F t)

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

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

1 subgoal (ID 96)
  
  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 (\cat_(t1<=t<t2)F t)

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

        
    - by rewrite !big_geq ⇒ //.

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

No more subgoals.

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

  Qed.

End BigCatNatLemmas.

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

Consider any two types supporting equality comparisons...
  Variable X Y : eqType.

...and a function that, given an index, yields a sequence.
  Variable f : X → seq Y.

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 :
      ∀ x y s,
      x \in s →
      y \in f x →
      y \in \cat_(x <- s) f x.

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

1 subgoal (ID 42)
  
  X, Y : eqType
  f : X -> seq Y
  ============================
  forall (x : X) (y : Y) (s : seq_predType X),
  x \in s -> y \in f x -> y \in \cat_(x0<-s)f x0

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

  Proof.
    move⇒ x y s INs INfx.

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

1 subgoal (ID 47)
  
  X, Y : eqType
  f : X -> seq Y
  x : X
  y : Y
  s : seq_predType X
  INs : x \in s
  INfx : y \in f x
  ============================
  y \in \cat_(x0<-s)f x0

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

    induction s; first by done.

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

1 subgoal (ID 64)
  
  X, Y : eqType
  f : X -> seq Y
  x : X
  y : Y
  a : X
  s : seq X
  INs : x \in a :: s
  INfx : y \in f x
  IHs : x \in s -> y \in \cat_(x<-s)f x
  ============================
  y \in \cat_(x0<-(a :: s))f x0

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

    rewrite big_cons mem_cat.

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

1 subgoal (ID 101)
  
  X, Y : eqType
  f : X -> seq Y
  x : X
  y : Y
  a : X
  s : seq X
  INs : x \in a :: s
  INfx : y \in f x
  IHs : x \in s -> y \in \cat_(x<-s)f x
  ============================
  (y \in f a) || (y \in \cat_(j<-s)f j)

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

    move:INs; rewrite in_cons ⇒ /orP[/eqP HEAD | CONS].

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

2 subgoals (ID 182)
  
  X, Y : eqType
  f : X -> seq Y
  x : X
  y : Y
  a : X
  s : seq X
  INfx : y \in f x
  IHs : x \in s -> y \in \cat_(x<-s)f x
  HEAD : x = a
  ============================
  (y \in f a) || (y \in \cat_(j<-s)f j)

subgoal 2 (ID 183) is:
 (y \in f a) || (y \in \cat_(j<-s)f j)

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

    - by rewrite -HEAD; apply /orP; left.

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

1 subgoal (ID 183)
  
  X, Y : eqType
  f : X -> seq Y
  x : X
  y : Y
  a : X
  s : seq X
  INfx : y \in f x
  IHs : x \in s -> y \in \cat_(x<-s)f x
  CONS : x \in s
  ============================
  (y \in f a) || (y \in \cat_(j<-s)f j)

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

    - by apply /orP; right; apply IHs.

(* ----------------------------------[ 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_exists :
    ∀ s y,
      y \in \cat_(x <- s) f x →
      ∃ x, x \in s ∧ y \in f x.

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

1 subgoal (ID 70)
  
  X, Y : eqType
  f : X -> seq Y
  ============================
  forall (s : seq X) (y : Y),
  y \in \cat_(x<-s)f x -> exists x : X, x \in s /\ y \in f x

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

  Proof.
    induction s; first by rewrite big_nil.

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

1 subgoal (ID 79)
  
  X, Y : eqType
  f : X -> seq Y
  a : X
  s : seq X
  IHs : forall y : Y,
        y \in \cat_(x<-s)f x -> exists x : X, x \in s /\ y \in f x
  ============================
  forall y : Y,
  y \in \cat_(x<-(a :: s))f x -> exists x : X, x \in a :: s /\ y \in f x

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

    move⇒ y.

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

1 subgoal (ID 118)
  
  X, Y : eqType
  f : X -> seq Y
  a : X
  s : seq X
  IHs : forall y : Y,
        y \in \cat_(x<-s)f x -> exists x : X, x \in s /\ y \in f x
  y : Y
  ============================
  y \in \cat_(x<-(a :: s))f x -> exists x : X, x \in a :: s /\ y \in f x

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

    rewrite big_cons mem_cat ⇒ /orP[HEAD | CONS].

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

2 subgoals (ID 176)
  
  X, Y : eqType
  f : X -> seq Y
  a : X
  s : seq X
  IHs : forall y : Y,
        y \in \cat_(x<-s)f x -> exists x : X, x \in s /\ y \in f x
  y : Y
  HEAD : y \in f a
  ============================
  exists x : X, x \in a :: s /\ y \in f x

subgoal 2 (ID 177) is:
 exists x : X, x \in a :: s /\ y \in f x

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

    - ∃ a.

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

2 subgoals (ID 179)
  
  X, Y : eqType
  f : X -> seq Y
  a : X
  s : seq X
  IHs : forall y : Y,
        y \in \cat_(x<-s)f x -> exists x : X, x \in s /\ y \in f x
  y : Y
  HEAD : y \in f a
  ============================
  a \in a :: s /\ y \in f a

subgoal 2 (ID 177) is:
 exists x : X, x \in a :: s /\ y \in f x

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

      by split ⇒ //; apply mem_head.

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

1 subgoal (ID 177)
  
  X, Y : eqType
  f : X -> seq Y
  a : X
  s : seq X
  IHs : forall y : Y,
        y \in \cat_(x<-s)f x -> exists x : X, x \in s /\ y \in f x
  y : Y
  CONS : y \in \cat_(j<-s)f j
  ============================
  exists x : X, x \in a :: s /\ y \in f x

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

    - move: (IHs _ CONS) ⇒ [x [INs INfx]].

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

1 subgoal (ID 227)
  
  X, Y : eqType
  f : X -> seq Y
  a : X
  s : seq X
  IHs : forall y : Y,
        y \in \cat_(x<-s)f x -> exists x : X, x \in s /\ y \in f x
  y : Y
  CONS : y \in \cat_(j<-s)f j
  x : X
  INs : x \in s
  INfx : y \in f x
  ============================
  exists x0 : X, x0 \in a :: s /\ y \in f x0

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

      ∃ x; split =>//.

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

1 subgoal (ID 231)
  
  X, Y : eqType
  f : X -> seq Y
  a : X
  s : seq X
  IHs : forall y : Y,
        y \in \cat_(x<-s)f x -> exists x : X, x \in s /\ y \in f x
  y : Y
  CONS : y \in \cat_(j<-s)f j
  x : X
  INs : x \in s
  INfx : y \in f x
  ============================
  x \in a :: s

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

      by rewrite in_cons; apply /orP; right.

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

No more subgoals.

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

  Qed.

Next, we show that a map and filter operation can be done either before or after a concatenation, leading to the same result.
  Lemma bigcat_filter_eq_filter_bigcat:
    ∀ xss P,
      [seq x <- \cat_(xs <- xss) f xs | P x] =
      \cat_(xs <- xss) [seq x <- f xs | P x] .

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

1 subgoal (ID 97)
  
  X, Y : eqType
  f : X -> seq Y
  ============================
  forall (xss : seq X) (P : Y -> bool),
  [seq x <- \cat_(xs<-xss)f xs | P x] = \cat_(xs<-xss)[seq x <- f xs | P x]

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

  Proof.
    move⇒ xss P.

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

1 subgoal (ID 99)
  
  X, Y : eqType
  f : X -> seq Y
  xss : seq X
  P : Y -> bool
  ============================
  [seq x <- \cat_(xs<-xss)f xs | P x] = \cat_(xs<-xss)[seq x <- f xs | P x]

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

    induction xss.

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

2 subgoals (ID 103)
  
  X, Y : eqType
  f : X -> seq Y
  P : Y -> bool
  ============================
  [seq x <- \cat_(xs<-[::])f xs | P x] = \cat_(xs<-[::])[seq x <- f xs | P x]

subgoal 2 (ID 109) is:
 [seq x <- \cat_(xs<-(a :: xss))f xs | P x] =
 \cat_(xs<-(a :: xss))[seq x <- f xs | P x]

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

    - by rewrite !big_nil.

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

1 subgoal (ID 109)
  
  X, Y : eqType
  f : X -> seq Y
  a : X
  xss : seq X
  P : Y -> bool
  IHxss : [seq x <- \cat_(xs<-xss)f xs | P x] =
          \cat_(xs<-xss)[seq x <- f xs | P x]
  ============================
  [seq x <- \cat_(xs<-(a :: xss))f xs | P x] =
  \cat_(xs<-(a :: xss))[seq x <- f xs | P x]

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

    - by rewrite !big_cons filter_cat IHxss.

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

No more subgoals.

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

  Qed.

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_f : ∀ x, uniq (f x).

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

We prove that the concatenation will yield a sequence with unique elements.
    Lemma bigcat_uniq :
      ∀ xs,
        uniq xs →
        uniq (\cat_(x <- xs) (f x)).

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

1 subgoal (ID 124)
  
  X, Y : eqType
  f : X -> seq Y
  H_uniq_f : forall x : X, uniq (f x)
  H_no_elements_in_common : forall (x : Y) (y z : X),
                            x \in f y -> x \in f z -> y = z
  ============================
  forall xs : seq X, uniq xs -> uniq (\cat_(x<-xs)f x)

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

    Proof.
      induction xs; first by rewrite big_nil.

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

1 subgoal (ID 133)
  
  X, Y : eqType
  f : X -> seq Y
  H_uniq_f : forall x : X, uniq (f x)
  H_no_elements_in_common : forall (x : Y) (y z : X),
                            x \in f y -> x \in f z -> y = z
  a : X
  xs : seq X
  IHxs : uniq xs -> uniq (\cat_(x<-xs)f x)
  ============================
  uniq (a :: xs) -> uniq (\cat_(x<-(a :: xs))f x)

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

      rewrite cons_uniq ⇒ /andP [NINxs UNIQ].

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

1 subgoal (ID 186)
  
  X, Y : eqType
  f : X -> seq Y
  H_uniq_f : forall x : X, uniq (f x)
  H_no_elements_in_common : forall (x : Y) (y z : X),
                            x \in f y -> x \in f z -> y = z
  a : X
  xs : seq X
  IHxs : uniq xs -> uniq (\cat_(x<-xs)f x)
  NINxs : a \notin xs
  UNIQ : uniq xs
  ============================
  uniq (\cat_(x<-(a :: xs))f x)

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

      rewrite big_cons cat_uniq.

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

1 subgoal (ID 201)
  
  X, Y : eqType
  f : X -> seq Y
  H_uniq_f : forall x : X, uniq (f x)
  H_no_elements_in_common : forall (x : Y) (y z : X),
                            x \in f y -> x \in f z -> y = z
  a : X
  xs : seq X
  IHxs : uniq xs -> uniq (\cat_(x<-xs)f x)
  NINxs : a \notin xs
  UNIQ : uniq xs
  ============================
  [&& uniq (f a), ~~ has (mem (f a)) (\cat_(j<-xs)f j)
    & uniq (\cat_(j<-xs)f j)]

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

      apply /andP; split; first by apply H_uniq_f.

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

1 subgoal (ID 228)
  
  X, Y : eqType
  f : X -> seq Y
  H_uniq_f : forall x : X, uniq (f x)
  H_no_elements_in_common : forall (x : Y) (y z : X),
                            x \in f y -> x \in f z -> y = z
  a : X
  xs : seq X
  IHxs : uniq xs -> uniq (\cat_(x<-xs)f x)
  NINxs : a \notin xs
  UNIQ : uniq xs
  ============================
  ~~ has (mem (f a)) (\cat_(j<-xs)f j) && uniq (\cat_(j<-xs)f j)

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

      apply /andP; split; last by apply IHxs.

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

1 subgoal (ID 254)
  
  X, Y : eqType
  f : X -> seq Y
  H_uniq_f : forall x : X, uniq (f x)
  H_no_elements_in_common : forall (x : Y) (y z : X),
                            x \in f y -> x \in f z -> y = z
  a : X
  xs : seq X
  IHxs : uniq xs -> uniq (\cat_(x<-xs)f x)
  NINxs : a \notin xs
  UNIQ : uniq xs
  ============================
  ~~ has (mem (f a)) (\cat_(j<-xs)f j)

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

      apply /hasPn⇒ x IN; apply /negP⇒ INfa.

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

1 subgoal (ID 309)
  
  X, Y : eqType
  f : X -> seq Y
  H_uniq_f : forall x : X, uniq (f x)
  H_no_elements_in_common : forall (x : Y) (y z : X),
                            x \in f y -> x \in f z -> y = z
  a : X
  xs : seq X
  IHxs : uniq xs -> uniq (\cat_(x<-xs)f x)
  NINxs : a \notin xs
  UNIQ : uniq xs
  x : Y
  IN : x \in \cat_(j<-xs)f j
  INfa : mem (f a) x
  ============================
  False

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

      move: (mem_bigcat_exists _ _ IN) ⇒ [a' [INxs INfa']].

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

1 subgoal (ID 335)
  
  X, Y : eqType
  f : X -> seq Y
  H_uniq_f : forall x : X, uniq (f x)
  H_no_elements_in_common : forall (x : Y) (y z : X),
                            x \in f y -> x \in f z -> y = z
  a : X
  xs : seq X
  IHxs : uniq xs -> uniq (\cat_(x<-xs)f x)
  NINxs : a \notin xs
  UNIQ : uniq xs
  x : Y
  IN : x \in \cat_(j<-xs)f j
  INfa : mem (f a) x
  a' : X
  INxs : a' \in xs
  INfa' : x \in f a'
  ============================
  False

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

      move: (H_no_elements_in_common x a a' INfa INfa') ⇒ EQa.

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

1 subgoal (ID 337)
  
  X, Y : eqType
  f : X -> seq Y
  H_uniq_f : forall x : X, uniq (f x)
  H_no_elements_in_common : forall (x : Y) (y z : X),
                            x \in f y -> x \in f z -> y = z
  a : X
  xs : seq X
  IHxs : uniq xs -> uniq (\cat_(x<-xs)f x)
  NINxs : a \notin xs
  UNIQ : uniq xs
  x : Y
  IN : x \in \cat_(j<-xs)f j
  INfa : mem (f a) x
  a' : X
  INxs : a' \in xs
  INfa' : x \in f a'
  EQa : a = a'
  ============================
  False

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

      by move: NINxs; rewrite EQa ⇒ /negP CONTRA.

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

No more subgoals.

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

    Qed.

  End BigCatDistinctElements.

In this section, we show some properties of the concatenation of sequences in combination with a function [g] that cancels [f].
  Section BigCatWithCancelFunctions.

Consider a function [g]...
    Variable g : Y → X.

... and assume that [g] can cancel [f] starting from an element of the sequence [f x].
    Hypothesis H_g_cancels_f : ∀ x y, y \in f x → g y = x.

First, we show that no element of a sequence [f x1] can be fed into [g] and obtain an element [x2] which differs from [x1]. Hence, filtering by this condition always leads to the empty sequence.
    Lemma seq_different_elements_nil :
      ∀ x1 x2,
        x1 != x2 →
        [seq x <- f x1 | g x == x2] = [::].

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

1 subgoal (ID 115)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  ============================
  forall x1 x2 : X, x1 != x2 -> [seq x <- f x1 | g x == x2] = [::]

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

    Proof.
      move ⇒ x1 x2 ⇒ /negP NEQ.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 142)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  x1, x2 : X
  NEQ : ~ x1 == x2
  ============================
  [seq x <- f x1 | g x == x2] = [::]

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

      apply filter_in_pred0.

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

1 subgoal (ID 144)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  x1, x2 : X
  NEQ : ~ x1 == x2
  ============================
  forall x : Y, x \in f x1 -> g x != x2

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

      move ⇒ y IN; apply/negP ⇒ /eqP EQ2.

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

1 subgoal (ID 200)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  x1, x2 : X
  NEQ : ~ x1 == x2
  y : Y
  IN : y \in f x1
  EQ2 : g y = x2
  ============================
  False

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

      apply: NEQ; apply/eqP.

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

1 focused subgoal
(shelved: 1) (ID 234)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  x1, x2 : X
  y : Y
  IN : y \in f x1
  EQ2 : g y = x2
  ============================
  x1 = x2

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

      move: (H_g_cancels_f _ _ IN) ⇒ EQ1.

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

1 subgoal (ID 240)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  x1, x2 : X
  y : Y
  IN : y \in f x1
  EQ2 : g y = x2
  EQ1 : g y = x1
  ============================
  x1 = x2

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

      by rewrite -EQ1 -EQ2.

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

No more subgoals.

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

    Qed.

Finally, assume we are given an element [y] which is contained in a duplicate-free sequence [xs]. Then, [f] is applied to each element of [xs], but only the elements for which [g] yields [y] are kept. In this scenario, concatenating the resulting sequences will always lead to [f y].
    Lemma bigcat_seq_uniqK :
      ∀ y xs,
        y \in xs →
        uniq xs →
        \cat_(x <- xs) [seq x' <- f x | g x' == y] = f y.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 140)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  ============================
  forall (y : X) (xs : seq_predType X),
  y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y

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

    Proof.
      move⇒ y xs IN UNI.

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

1 subgoal (ID 144)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  y : X
  xs : seq_predType X
  IN : y \in xs
  UNI : uniq xs
  ============================
  \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y

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

      induction xs as [ | x' xs]; first by done.

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

1 subgoal (ID 163)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  y, x' : X
  xs : seq X
  IN : y \in x' :: xs
  UNI : uniq (x' :: xs)
  IHxs : y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
  ============================
  \cat_(x<-(x' :: xs))[seq x'0 <- f x | g x'0 == y] = f y

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

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

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

2 subgoals (ID 265)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  y, x' : X
  xs : seq X
  UNI : uniq (x' :: xs)
  IHxs : y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
  EQ : y = x'
  ============================
  \cat_(x<-(x' :: xs))[seq x'0 <- f x | g x'0 == y] = f y

subgoal 2 (ID 266) is:
 \cat_(x<-(x' :: xs))[seq x'0 <- f x | g x'0 == y] = f y

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

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

1 subgoal (ID 265)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  y, x' : X
  xs : seq X
  UNI : uniq (x' :: xs)
  IHxs : y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
  EQ : y = x'
  ============================
  \cat_(x<-(x' :: xs))[seq x'0 <- f x | g x'0 == y] = f y

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

subst; rewrite !big_cons.

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

1 subgoal (ID 282)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  x' : X
  xs : seq X
  UNI : uniq (x' :: xs)
  IHxs : x' \in xs ->
         uniq xs -> \cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] = f x'
  ============================
  [seq x'0 <- f x' | g x'0 == x'] ++
  \cat_(j<-xs)[seq x'0 <- f j | g x'0 == x'] = f x'

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

        have → : [seq x <- f x' | g x == x'] = f x'.

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

2 subgoals (ID 295)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  x' : X
  xs : seq X
  UNI : uniq (x' :: xs)
  IHxs : x' \in xs ->
         uniq xs -> \cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] = f x'
  ============================
  [seq x <- f x' | g x == x'] = f x'

subgoal 2 (ID 300) is:
 f x' ++ \cat_(j<-xs)[seq x'0 <- f j | g x'0 == x'] = f x'

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

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

1 subgoal (ID 295)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  x' : X
  xs : seq X
  UNI : uniq (x' :: xs)
  IHxs : x' \in xs ->
         uniq xs -> \cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] = f x'
  ============================
  [seq x <- f x' | g x == x'] = f x'

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

apply/all_filterP/allP.

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

1 focused subgoal
(shelved: 1) (ID 423)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  x' : X
  xs : seq X
  UNI : uniq (x' :: xs)
  IHxs : x' \in xs ->
         uniq xs -> \cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] = f x'
  ============================
  {in f x', forall x : Y, g x == x'}

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

          intros y IN; apply/eqP.

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

1 focused subgoal
(shelved: 1) (ID 454)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  x' : X
  xs : seq X
  UNI : uniq (x' :: xs)
  IHxs : x' \in xs ->
         uniq xs -> \cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] = f x'
  y : Y
  IN : y \in f x'
  ============================
  g y = x'

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

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

2 subgoals

subgoal 1 (ID 300) is:
 f x' ++ \cat_(j<-xs)[seq x'0 <- f j | g x'0 == x'] = f x'
subgoal 2 (ID 266) is:
 \cat_(x<-(x' :: xs))[seq x'0 <- f x | g x'0 == y] = f y

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

}

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

1 subgoal (ID 300)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  x' : X
  xs : seq X
  UNI : uniq (x' :: xs)
  IHxs : x' \in xs ->
         uniq xs -> \cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] = f x'
  ============================
  f x' ++ \cat_(j<-xs)[seq x'0 <- f j | g x'0 == x'] = f x'

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

        have ->: \cat_(j<-xs)[seq x <- f j | g x == x'] = [::]; last by rewrite cats0.

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

1 subgoal (ID 468)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  x' : X
  xs : seq X
  UNI : uniq (x' :: xs)
  IHxs : x' \in xs ->
         uniq xs -> \cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] = f x'
  ============================
  \cat_(j<-xs)[seq x <- f j | g x == x'] = [::]

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

        rewrite big1_seq //; move ⇒ xs2 /andP [_ IN].

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

1 subgoal (ID 554)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  x' : X
  xs : seq X
  UNI : uniq (x' :: xs)
  IHxs : x' \in xs ->
         uniq xs -> \cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] = f x'
  xs2 : X
  IN : xs2 \in xs
  ============================
  [seq x <- f xs2 | g x == x'] = [::]

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

        have NEQ: xs2 != x'; last by rewrite seq_different_elements_nil.

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

1 subgoal (ID 556)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  x' : X
  xs : seq X
  UNI : uniq (x' :: xs)
  IHxs : x' \in xs ->
         uniq xs -> \cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] = f x'
  xs2 : X
  IN : xs2 \in xs
  ============================
  xs2 != x'

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

        apply/neqP; intros EQ; subst x'.

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

1 subgoal (ID 599)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  xs : seq X
  xs2 : X
  IHxs : xs2 \in xs ->
         uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == xs2] = f xs2
  UNI : uniq (xs2 :: xs)
  IN : xs2 \in xs
  ============================
  False

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

        move: UNI; rewrite cons_uniq ⇒ /andP [NIN _].

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

1 subgoal (ID 645)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  xs : seq X
  xs2 : X
  IHxs : xs2 \in xs ->
         uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == xs2] = f xs2
  IN : xs2 \in xs
  NIN : xs2 \notin xs
  ============================
  False

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

        by move: NIN ⇒ /negP NIN; apply: NIN.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 266) is:
 \cat_(x<-(x' :: xs))[seq x'0 <- f x | g x'0 == y] = f y

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

}

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

1 subgoal (ID 266)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  y, x' : X
  xs : seq X
  UNI : uniq (x' :: xs)
  IHxs : y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
  IN : y \in xs
  ============================
  \cat_(x<-(x' :: xs))[seq x'0 <- f x | g x'0 == y] = f y

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

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

1 subgoal (ID 266)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  y, x' : X
  xs : seq X
  UNI : uniq (x' :: xs)
  IHxs : y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
  IN : y \in xs
  ============================
  \cat_(x<-(x' :: xs))[seq x'0 <- f x | g x'0 == y] = f y

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

rewrite big_cons IHxs //; last by move:UNI; rewrite cons_uniq⇒ /andP[_ ?].

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

1 subgoal (ID 692)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  y, x' : X
  xs : seq X
  UNI : uniq (x' :: xs)
  IHxs : y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
  IN : y \in xs
  ============================
  [seq x'0 <- f x' | g x'0 == y] ++ f y = f y

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

        have NEQ: (x' != y); last by rewrite seq_different_elements_nil.

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

1 subgoal (ID 784)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  y, x' : X
  xs : seq X
  UNI : uniq (x' :: xs)
  IHxs : y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
  IN : y \in xs
  ============================
  x' != y

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

        apply/neqP; intros EQ; subst x'.

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

1 subgoal (ID 825)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  y : X
  xs : seq X
  UNI : uniq (y :: xs)
  IHxs : y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
  IN : y \in xs
  ============================
  False

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

        move: UNI; rewrite cons_uniq ⇒ /andP [NIN _].

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

1 subgoal (ID 871)
  
  X, Y : eqType
  f : X -> seq Y
  g : Y -> X
  H_g_cancels_f : forall (x : X) (y : Y), y \in f x -> g y = x
  y : X
  xs : seq X
  IHxs : y \in xs -> uniq xs -> \cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
  IN : y \in xs
  NIN : y \notin xs
  ============================
  False

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

        by move: NIN ⇒ /negP NIN; apply: NIN.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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

}

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

No more subgoals.

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

    Qed.

  End BigCatWithCancelFunctions.

End BigCatLemmas.

In this section, we show that the number of elements of the result of a nested mapping and concatenation operation is independent from the order in which the concatenations are performed.
Section BigCatNestedCount.

Consider any three types supporting equality comparisons...
  Variable X Y Z : eqType.

... a function [F] that, given two indices, yields a sequence...
  Variable F : X → Y → seq Z.

and a predicate [P].
  Variable P : pred Z.

Assume that, given two sequences [xs] and [ys], their elements are fed to [F] in a pair-wise fashion. The resulting lists are then concatenated. The following lemma shows that, when the operation described above is performed, the number of elements respecting [P] in the resulting list is the same, regardless of the order in which [xs] and [ys] are combined.
  Lemma bigcat_count_exchange :
    ∀ xs ys,
      count P (\cat_(x <- xs) \cat_(y <- ys) F x y) =
      count P (\cat_(y <- ys) \cat_(x <- xs) F x y).
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 53)
  
  X, Y, Z : eqType
  F : X -> Y -> seq Z
  P : pred Z
  ============================
  forall (xs : seq X) (ys : seq Y),
  count P (\cat_(x<-xs)\cat_(y<-ys)F x y) =
  count P (\cat_(y<-ys)\cat_(x<-xs)F x y)

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

  Proof.
    induction xs as [|x0 seqX IHxs]; induction ys as [|y0 seqY IHys]; intros.

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

4 subgoals (ID 67)
  
  X, Y, Z : eqType
  F : X -> Y -> seq Z
  P : pred Z
  ============================
  count P (\cat_(x<-[::])\cat_(y<-[::])F x y) =
  count P (\cat_(y<-[::])\cat_(x<-[::])F x y)

subgoal 2 (ID 71) is:
 count P (\cat_(x<-[::])\cat_(y<-(y0 :: seqY))F x y) =
 count P (\cat_(y<-(y0 :: seqY))\cat_(x<-[::])F x y)
subgoal 3 (ID 76) is:
 count P (\cat_(x<-(x0 :: seqX))\cat_(y<-[::])F x y) =
 count P (\cat_(y<-[::])\cat_(x<-(x0 :: seqX))F x y)
subgoal 4 (ID 80) is:
 count P (\cat_(x<-(x0 :: seqX))\cat_(y<-(y0 :: seqY))F x y) =
 count P (\cat_(y<-(y0 :: seqY))\cat_(x<-(x0 :: seqX))F x y)

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

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

1 subgoal (ID 67)
  
  X, Y, Z : eqType
  F : X -> Y -> seq Z
  P : pred Z
  ============================
  count P (\cat_(x<-[::])\cat_(y<-[::])F x y) =
  count P (\cat_(y<-[::])\cat_(x<-[::])F x y)

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

by rewrite !big_nil.
(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals

subgoal 1 (ID 71) is:
 count P (\cat_(x<-[::])\cat_(y<-(y0 :: seqY))F x y) =
 count P (\cat_(y<-(y0 :: seqY))\cat_(x<-[::])F x y)
subgoal 2 (ID 76) is:
 count P (\cat_(x<-(x0 :: seqX))\cat_(y<-[::])F x y) =
 count P (\cat_(y<-[::])\cat_(x<-(x0 :: seqX))F x y)
subgoal 3 (ID 80) is:
 count P (\cat_(x<-(x0 :: seqX))\cat_(y<-(y0 :: seqY))F x y) =
 count P (\cat_(y<-(y0 :: seqY))\cat_(x<-(x0 :: seqX))F x y)

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

}

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

3 subgoals (ID 71)
  
  X, Y, Z : eqType
  F : X -> Y -> seq Z
  P : pred Z
  y0 : Y
  seqY : seq Y
  IHys : count P (\cat_(x<-[::])\cat_(y<-seqY)F x y) =
         count P (\cat_(y<-seqY)\cat_(x<-[::])F x y)
  ============================
  count P (\cat_(x<-[::])\cat_(y<-(y0 :: seqY))F x y) =
  count P (\cat_(y<-(y0 :: seqY))\cat_(x<-[::])F x y)

subgoal 2 (ID 76) is:
 count P (\cat_(x<-(x0 :: seqX))\cat_(y<-[::])F x y) =
 count P (\cat_(y<-[::])\cat_(x<-(x0 :: seqX))F x y)
subgoal 3 (ID 80) is:
 count P (\cat_(x<-(x0 :: seqX))\cat_(y<-(y0 :: seqY))F x y) =
 count P (\cat_(y<-(y0 :: seqY))\cat_(x<-(x0 :: seqX))F x y)

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

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

1 subgoal (ID 71)
  
  X, Y, Z : eqType
  F : X -> Y -> seq Z
  P : pred Z
  y0 : Y
  seqY : seq Y
  IHys : count P (\cat_(x<-[::])\cat_(y<-seqY)F x y) =
         count P (\cat_(y<-seqY)\cat_(x<-[::])F x y)
  ============================
  count P (\cat_(x<-[::])\cat_(y<-(y0 :: seqY))F x y) =
  count P (\cat_(y<-(y0 :: seqY))\cat_(x<-[::])F x y)

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

by rewrite big_cons count_cat -IHys !big_nil.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals

subgoal 1 (ID 76) is:
 count P (\cat_(x<-(x0 :: seqX))\cat_(y<-[::])F x y) =
 count P (\cat_(y<-[::])\cat_(x<-(x0 :: seqX))F x y)
subgoal 2 (ID 80) is:
 count P (\cat_(x<-(x0 :: seqX))\cat_(y<-(y0 :: seqY))F x y) =
 count P (\cat_(y<-(y0 :: seqY))\cat_(x<-(x0 :: seqX))F x y)

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

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

2 subgoals (ID 76)
  
  X, Y, Z : eqType
  F : X -> Y -> seq Z
  P : pred Z
  x0 : X
  seqX : seq X
  IHxs : forall ys : seq Y,
         count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) =
         count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)
  ============================
  count P (\cat_(x<-(x0 :: seqX))\cat_(y<-[::])F x y) =
  count P (\cat_(y<-[::])\cat_(x<-(x0 :: seqX))F x y)

subgoal 2 (ID 80) is:
 count P (\cat_(x<-(x0 :: seqX))\cat_(y<-(y0 :: seqY))F x y) =
 count P (\cat_(y<-(y0 :: seqY))\cat_(x<-(x0 :: seqX))F x y)

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


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

1 subgoal (ID 76)
  
  X, Y, Z : eqType
  F : X -> Y -> seq Z
  P : pred Z
  x0 : X
  seqX : seq X
  IHxs : forall ys : seq Y,
         count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) =
         count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)
  ============================
  count P (\cat_(x<-(x0 :: seqX))\cat_(y<-[::])F x y) =
  count P (\cat_(y<-[::])\cat_(x<-(x0 :: seqX))F x y)

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

by rewrite big_cons count_cat IHxs !big_nil.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 80) is:
 count P (\cat_(x<-(x0 :: seqX))\cat_(y<-(y0 :: seqY))F x y) =
 count P (\cat_(y<-(y0 :: seqY))\cat_(x<-(x0 :: seqX))F x y)

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

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

1 subgoal (ID 80)
  
  X, Y, Z : eqType
  F : X -> Y -> seq Z
  P : pred Z
  x0 : X
  seqX : seq X
  IHxs : forall ys : seq Y,
         count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) =
         count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)
  y0 : Y
  seqY : seq Y
  IHys : count P (\cat_(x<-(x0 :: seqX))\cat_(y<-seqY)F x y) =
         count P (\cat_(y<-seqY)\cat_(x<-(x0 :: seqX))F x y)
  ============================
  count P (\cat_(x<-(x0 :: seqX))\cat_(y<-(y0 :: seqY))F x y) =
  count P (\cat_(y<-(y0 :: seqY))\cat_(x<-(x0 :: seqX))F x y)

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


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

1 subgoal (ID 80)
  
  X, Y, Z : eqType
  F : X -> Y -> seq Z
  P : pred Z
  x0 : X
  seqX : seq X
  IHxs : forall ys : seq Y,
         count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) =
         count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)
  y0 : Y
  seqY : seq Y
  IHys : count P (\cat_(x<-(x0 :: seqX))\cat_(y<-seqY)F x y) =
         count P (\cat_(y<-seqY)\cat_(x<-(x0 :: seqX))F x y)
  ============================
  count P (\cat_(x<-(x0 :: seqX))\cat_(y<-(y0 :: seqY))F x y) =
  count P (\cat_(y<-(y0 :: seqY))\cat_(x<-(x0 :: seqX))F x y)

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

rewrite !big_cons !count_cat.

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

1 subgoal (ID 271)
  
  X, Y, Z : eqType
  F : X -> Y -> seq Z
  P : pred Z
  x0 : X
  seqX : seq X
  IHxs : forall ys : seq Y,
         count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) =
         count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)
  y0 : Y
  seqY : seq Y
  IHys : count P (\cat_(x<-(x0 :: seqX))\cat_(y<-seqY)F x y) =
         count P (\cat_(y<-seqY)\cat_(x<-(x0 :: seqX))F x y)
  ============================
  count P (F x0 y0) + count P (\cat_(j<-seqY)F x0 j) +
  count P (\cat_(j<-seqX)\cat_(y<-(y0 :: seqY))F j y) =
  count P (F x0 y0) + count P (\cat_(j<-seqX)F j y0) +
  count P (\cat_(j<-seqY)\cat_(x<-(x0 :: seqX))F x j)

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

      apply/eqP; rewrite -!addnA eqn_add2l.

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

1 subgoal (ID 354)
  
  X, Y, Z : eqType
  F : X -> Y -> seq Z
  P : pred Z
  x0 : X
  seqX : seq X
  IHxs : forall ys : seq Y,
         count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) =
         count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)
  y0 : Y
  seqY : seq Y
  IHys : count P (\cat_(x<-(x0 :: seqX))\cat_(y<-seqY)F x y) =
         count P (\cat_(y<-seqY)\cat_(x<-(x0 :: seqX))F x y)
  ============================
  count P (\cat_(j<-seqY)F x0 j) +
  count P (\cat_(j<-seqX)\cat_(y<-(y0 :: seqY))F j y) ==
  count P (\cat_(j<-seqX)F j y0) +
  count P (\cat_(j<-seqY)\cat_(x<-(x0 :: seqX))F x j)

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

      rewrite IHxs -IHys !big_cons !count_cat.

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

1 subgoal (ID 399)
  
  X, Y, Z : eqType
  F : X -> Y -> seq Z
  P : pred Z
  x0 : X
  seqX : seq X
  IHxs : forall ys : seq Y,
         count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) =
         count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)
  y0 : Y
  seqY : seq Y
  IHys : count P (\cat_(x<-(x0 :: seqX))\cat_(y<-seqY)F x y) =
         count P (\cat_(y<-seqY)\cat_(x<-(x0 :: seqX))F x y)
  ============================
  count P (\cat_(j<-seqY)F x0 j) +
  (count P (\cat_(x<-seqX)F x y0) +
   count P (\cat_(j<-seqY)\cat_(x<-seqX)F x j)) ==
  count P (\cat_(j<-seqX)F j y0) +
  (count P (\cat_(y<-seqY)F x0 y) +
   count P (\cat_(j<-seqX)\cat_(y<-seqY)F j y))

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

      rewrite addnC -!addnA eqn_add2l addnC eqn_add2l.

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

1 subgoal (ID 437)
  
  X, Y, Z : eqType
  F : X -> Y -> seq Z
  P : pred Z
  x0 : X
  seqX : seq X
  IHxs : forall ys : seq Y,
         count P (\cat_(x<-seqX)\cat_(y<-ys)F x y) =
         count P (\cat_(y<-ys)\cat_(x<-seqX)F x y)
  y0 : Y
  seqY : seq Y
  IHys : count P (\cat_(x<-(x0 :: seqX))\cat_(y<-seqY)F x y) =
         count P (\cat_(y<-seqY)\cat_(x<-(x0 :: seqX))F x y)
  ============================
  count P (\cat_(j<-seqY)\cat_(x<-seqX)F x j) ==
  count P (\cat_(j<-seqX)\cat_(y<-seqY)F j y)

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

      by rewrite IHxs.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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

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

No more subgoals.

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


  Qed.

End BigCatNestedCount.