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

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

  (** Consider any type [T] supporting equality comparisons... *)
  Variable T : eqType.

  (** ...and a function [f] that, given an index, yields a sequence. *)
  Variable f : nat -> seq 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 :
      forall x m n j,
        m <= j < n ->
        x \in f j ->
        x \in \cat_(m <= i < n) (f i).
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.
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
      intros x m n j LE IN; move: LE => /andP [LE LE0].
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].
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.
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.
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.
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.
    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 :
      forall x m n,
        x \in \cat_(m <= i < n) (f i) ->
        exists i,
          x \in f i /\ m <= i < n.
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.
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
      intros x m n IN.
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
      elim: n IN => [|n IHn] IN; first by rewrite big_geq // in IN.
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
IN: x \in \cat_(m<=i<n.+1)f i
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.
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
IN: x \in \cat_(m<=i<n.+1)f i
i: m <= n
exists i : nat, x \in f i /\ m <= i < n.+1
      rewrite big_nat_recr // /= mem_cat in IN.
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 i : nat, x \in f i /\ m <= i < n.+1
      move: IN => /orP [HEAD | TAIL].
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 i : nat, x \in f i /\ m <= i < n.+1
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 i : nat, x \in f i /\ m <= i < n.+1
      -
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 i : nat, x \in f i /\ m <= i < n.+1 move: (IHn HEAD) => [x0 [H /andP[H0 H1]]]; exists x0.
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
x0: nat
H: x \in f x0
H0: m <= x0
H1: x0 < n
x \in f x0 /\ m <= x0 < n.+1
        split; first by done.
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
x0: nat
H: x \in f x0
H0: m <= x0
H1: x0 < n
m <= x0 < n.+1
        by apply/andP; split; last by apply ltnW.
      -
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 i : nat, x \in f i /\ m <= i < n.+1 exists n; split; first by done.
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.
    Qed.

    (** We also restate lemma [mem_bigcat_nat] in terms of ordinals. *)
    Lemma mem_bigcat_ord :
      forall (x : T) (n : nat) (j : 'I_n) (f : 'I_n -> seq T),
        j < n ->
        x \in (f j) ->
        x \in \cat_(i < n) (f i).
T: eqType
f: nat -> seq T
forall (x : T) (n : nat) (j : 'I_n)
  (f : 'I_n -> seq T),
j < n -> x \in f j -> x \in \cat_(i<n)f i
    Proof.
T: eqType
f: nat -> seq T
forall (x : T) (n : nat) (j : 'I_n)
  (f : 'I_n -> seq T),
j < n -> x \in f j -> x \in \cat_(i<n)f i
      move=> x; elim=> [//|n IHn] j f' Hj Hx.
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.
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].
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
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
      -
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 by right; rewrite (_ : ord_max = j); [|apply ord_inj].
      -
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.
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 []|].
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|].
    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 : forall i, uniq (f i).

    (** ...and that there are no elements in common between the sequences. *)
    Hypothesis H_no_elements_in_common :
      forall 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 :
      forall n1 n2,
        uniq (\cat_(n1 <= i < n2) (f i)).
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.
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)
      intros n1 n2.
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.
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).
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.
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)
      elim: delta => [|delta IHdelta]; first by rewrite addn0 big_geq.
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.
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.
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 [in \cat_(n1<=i<n1 + delta)f i] (f (n1 + delta)) &&
uniq (f (n1 + delta))
      apply /andP; split; last by apply H_uniq_seq.
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 [in \cat_(n1<=i<n1 + delta)f i] (f (n1 + delta))
      rewrite -all_predC; apply/allP; intros x INx.
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 \cat_(n1<=i<n1 + delta)f i] x
      simpl; apply/negP; unfold not; intro BUG.
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.
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]]].
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.
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.
    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 :
      forall (n : nat) (f : 'I_n -> seq T),
        uniq (\cat_(i < n) (f i)) ->
        (forall x i1 i2,
            x \in (f i1) -> x \in (f i2) -> i1 = i2).
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) (f : 'I_n -> seq T),
uniq (\cat_(i<n)f i) ->
forall (x : T) (i1 i2 : 'I_n),
x \in f i1 -> x \in f i2 -> i1 = i2
    Proof.
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) (f : 'I_n -> seq T),
uniq (\cat_(i<n)f i) ->
forall (x : T) (i1 i2 : 'I_n),
x \in f i1 -> x \in f i2 -> i1 = i2
      case=> [|n]; [by move=> f' Huniq x; case|].
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 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
      elim: n => [|n IHn] f' Huniq x i1 i2 Hi1 Hi2.
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
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
      {
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|//].
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. }
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].
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
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
      all: move: (leq_ord i2); rewrite leq_eqVlt => /orP [H'i2|H'i2].
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
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
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
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
      {
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 ->. }
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
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
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
      {
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.
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 _]].
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
  [in \big[seq_cat__canonical__Monoid_Law 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.
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
  [in \big[seq_cat__canonical__Monoid_Law T/[::]]_(i < n.+1) 
      f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)]
  (f' ord_max)
        apply /hasP; exists x => /=.
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
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)
        {
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 []|].
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 ->. }
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)) => //.
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]. }
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
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
      {
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.
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 _]].
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
  [in \big[seq_cat__canonical__Monoid_Law 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.
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
  [in \big[seq_cat__canonical__Monoid_Law T/[::]]_(i < n.+1) 
      f' (widen_ord (m:=n.+2) (leqnSn n.+1) i)]
  (f' ord_max)
        apply /hasP; exists x => /=.
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
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)
        {
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 []|].
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 ->. }
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)) => //.
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]. }
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 _].
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[seq_cat__canonical__Monoid_Law 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.
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[seq_cat__canonical__Monoid_Law T/[::]]_(i < n.+1) 
   f' (widen_ord (m:=n.+2) (leqnSn n.+1) i))
inord i1 = inord i2
      apply (IHn _ Huniq x).
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[seq_cat__canonical__Monoid_Law 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))
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[seq_cat__canonical__Monoid_Law 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))
      {
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[seq_cat__canonical__Monoid_Law 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 []|].
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[seq_cat__canonical__Monoid_Law 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. }
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[seq_cat__canonical__Monoid_Law 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 []|].
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[seq_cat__canonical__Monoid_Law 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.
    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 :
    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].
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.
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]
    move=> X F P t1 t2.
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].
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]
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]
    +
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] have EX: exists Δ, t2 = t1 + Δ by simpl; exists (t2 - t1); lia.
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]
      move: EX => [Δ EQ]; subst t2.
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]
      elim: Δ T1_LT => [|Δ IHΔ] T1_LT.
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]
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
P: X -> bool
t1, Δ: nat
IHΔ: t1 <= t1 + Δ ->
[seq x <- \cat_(t1<=t<t1 + Δ)F t | P x] =
\cat_(t1<=t<t1 + Δ)[seq x <- F t | P x]
T1_LT: t1 <= t1 + Δ.+1
[seq x <- \cat_(t1<=t<t1 + Δ.+1)F t | P x] =
\cat_(t1<=t<t1 + Δ.+1)[seq x <- F t | P x]
      {
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 => //. }
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
P: X -> bool
t1, Δ: nat
IHΔ: t1 <= t1 + Δ ->
[seq x <- \cat_(t1<=t<t1 + Δ)F t | P x] =
\cat_(t1<=t<t1 + Δ)[seq x <- F t | P x]
T1_LT: t1 <= t1 + Δ.+1
[seq x <- \cat_(t1<=t<t1 + Δ.+1)F t | P x] =
\cat_(t1<=t<t1 + Δ.+1)[seq x <- F t | P x]
      {
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
P: X -> bool
t1, Δ: nat
IHΔ: t1 <= t1 + Δ ->
[seq x <- \cat_(t1<=t<t1 + Δ)F t | P x] =
\cat_(t1<=t<t1 + Δ)[seq x <- F t | P x]
T1_LT: t1 <= t1 + Δ.+1
[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.
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
P: X -> bool
t1, Δ: nat
IHΔ: t1 <= t1 + Δ ->
[seq x <- \cat_(t1<=t<t1 + Δ)F t | P x] =
\cat_(t1<=t<t1 + Δ)[seq x <- F t | P x]
T1_LT: t1 <= t1 + Δ.+1
[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Δ => //.
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
P: X -> bool
t1, Δ: nat
IHΔ: t1 <= t1 + Δ ->
[seq x <- \cat_(t1<=t<t1 + Δ)F t | P x] =
\cat_(t1<=t<t1 + Δ)[seq x <- F t | P x]
T1_LT: t1 <= t1 + Δ.+1
t1 <= t1 + Δ
        by lia. }
    +
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 => //.
  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 : 
    forall {X : Type} (F : nat -> seq X) (t1 t2 : nat),
      \sum_(t1 <= t < t2) size (F t) =
      size (\cat_(t1 <= t < t2) F t).
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.
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)
    move=> X F t1 t2.
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].
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)
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)
    -
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) have EX: exists Δ, t2 = t1 + Δ by simpl; exists (t2 - t1); lia.
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)
      move: EX => [Δ EQ]; subst t2.
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)
      elim: Δ T1_LT => [|Δ IHΔ] T1_LT.
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)
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
t1, Δ: nat
IHΔ: t1 <= t1 + Δ ->
\sum_(t1 <= t < t1 + Δ) size (F t) =
size (\cat_(t1<=t<t1 + Δ)F t)
T1_LT: t1 <= t1 + Δ.+1
\sum_(t1 <= t < t1 + Δ.+1) size (F t) =
size (\cat_(t1<=t<t1 + Δ.+1)F t)
      {
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 => //. }
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
t1, Δ: nat
IHΔ: t1 <= t1 + Δ ->
\sum_(t1 <= t < t1 + Δ) size (F t) = size (\cat_(t1<=t<t1 + Δ)F t)
T1_LT: t1 <= t1 + Δ.+1
\sum_(t1 <= t < t1 + Δ.+1) size (F t) =
size (\cat_(t1<=t<t1 + Δ.+1)F t)
      {
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
t1, Δ: nat
IHΔ: t1 <= t1 + Δ ->
\sum_(t1 <= t < t1 + Δ) size (F t) = size (\cat_(t1<=t<t1 + Δ)F t)
T1_LT: t1 <= t1 + Δ.+1
\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.
T: eqType
f: nat -> seq T
X: Type
F: nat -> seq X
t1, Δ: nat
IHΔ: t1 <= t1 + Δ ->
\sum_(t1 <= t < t1 + Δ) size (F t) = size (\cat_(t1<=t<t1 + Δ)F t)
T1_LT: t1 <= t1 + Δ.+1
\sum_(t1 <= i < t1 + Δ) size (F i) + size (F (t1 + Δ)) =
size (\cat_(t1<=i<t1 + Δ)F i ++ F (t1 + Δ))
        by rewrite size_cat IHΔ => //; lia. }         
    -
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 => //.
  Qed.      
  
End BigCatNatLemmas.


(** In this section, we introduce a few lemmas about the concatenation
    operation performed over arbitrary sequences. *)
Section BigCatLemmas.

  (** Consider any two types [X] and [Y] supporting equality comparisons... *)
  Variable X Y : eqType.

  (** ...and a function [f] that, given an index [X], yields a sequence of [Y]. *)
  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 :
      forall x y s, 
      x \in s ->
      y \in f x -> 
      y \in \cat_(x <- s) f x.
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.
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
    move=> x y s INs INfx.
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_(x<-s)f x
    elim: s INs => [//|z s IHs] INs.
X, Y: eqType
f: X -> seq Y
x: X
y: Y
INfx: y \in f x
z: X
s: seq X
IHs: x \in s -> y \in \cat_(x<-s)f x
INs: x \in z :: s
y \in \cat_(x<-(z :: s))f x
    rewrite big_cons mem_cat.
X, Y: eqType
f: X -> seq Y
x: X
y: Y
INfx: y \in f x
z: X
s: seq X
IHs: x \in s -> y \in \cat_(x<-s)f x
INs: x \in z :: s
(y \in f z) || (y \in \cat_(j<-s)f j)
    move:INs; rewrite in_cons => /orP[/eqP HEAD | CONS].
X, Y: eqType
f: X -> seq Y
x: X
y: Y
INfx: y \in f x
z: X
s: seq X
IHs: x \in s -> y \in \cat_(x<-s)f x
HEAD: x = z
(y \in f z) || (y \in \cat_(j<-s)f j)
X, Y: eqType
f: X -> seq Y
x: X
y: Y
INfx: y \in f x
z: X
s: seq X
IHs: x \in s -> y \in \cat_(x<-s)f x
CONS: x \in s
(y \in f z) || (y \in \cat_(j<-s)f j)
    -
X, Y: eqType
f: X -> seq Y
x: X
y: Y
INfx: y \in f x
z: X
s: seq X
IHs: x \in s -> y \in \cat_(x<-s)f x
HEAD: x = z
(y \in f z) || (y \in \cat_(j<-s)f j) by rewrite -HEAD; apply /orP; left.
    -
X, Y: eqType
f: X -> seq Y
x: X
y: Y
INfx: y \in f x
z: X
s: seq X
IHs: x \in s -> y \in \cat_(x<-s)f x
CONS: x \in s
(y \in f z) || (y \in \cat_(j<-s)f j) by apply /orP; right; apply IHs.
  Qed.

  (** Conversely, we prove that any element belonging to a concatenation of sequences 
      must come from one of the sequences. *)
  Lemma mem_bigcat_exists :
    forall {P} s y,
      y \in \cat_(x <- s | P x) f x ->
      exists x, x \in s /\ y \in f x.
X, Y: eqType
f: X -> seq Y
forall (P : X -> bool) (s : seq X) (y : Y),
y \in \cat_(x<-s|P x)f x ->
exists x : X, x \in s /\ y \in f x
  Proof.
X, Y: eqType
f: X -> seq Y
forall (P : X -> bool) (s : seq X) (y : Y),
y \in \cat_(x<-s|P x)f x ->
exists x : X, x \in s /\ y \in f x
    move=> P.
X, Y: eqType
f: X -> seq Y
P: X -> bool
forall (s : seq X) (y : Y),
y \in \cat_(x<-s|P x)f x ->
exists x : X, x \in s /\ y \in f x
    elim=> [|a s IHs] y; first by rewrite big_nil.
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y, y \in \cat_(x<-s|P x)f x -> exists x : X, x \in s /\ y \in f x
y: Y
y \in \cat_(x<-(a :: s)|P x)f x ->
exists x : X, x \in a :: s /\ y \in f x
    rewrite big_cons.
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y, y \in \cat_(x<-s|P x)f x -> exists x : X, x \in s /\ y \in f x
y: Y
y
  \in (if P a
       then f a ++ \cat_(j<-s|P j)f j
       else \cat_(j<-s|P j)f j) ->
exists x : X, x \in a :: s /\ y \in f x
    case: (P a) => [|IN];
      last by move: (IHs y IN) => [x [INx INy]]; exists x; split => //; rewrite in_cons INx orbT.
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y, y \in \cat_(x<-s|P x)f x -> exists x : X, x \in s /\ y \in f x
y: Y
y \in f a ++ \cat_(j<-s|P j)f j ->
exists x : X, x \in a :: s /\ y \in f x
    rewrite mem_cat => /orP[HEAD | CONS].
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y, y \in \cat_(x<-s|P x)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
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y,
y \in \cat_(x<-s|P x)f x ->
exists x : X, x \in s /\ y \in f x
y: Y
CONS: y \in \cat_(j<-s|P j)f j
exists x : X, x \in a :: s /\ y \in f x
    -
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y, y \in \cat_(x<-s|P x)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 exists a.
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y, y \in \cat_(x<-s|P x)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
      by split => //; apply mem_head.
    -
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y, y \in \cat_(x<-s|P x)f x -> exists x : X, x \in s /\ y \in f x
y: Y
CONS: y \in \cat_(j<-s|P j)f j
exists x : X, x \in a :: s /\ y \in f x move: (IHs _ CONS) => [x [INs INfx]].
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y, y \in \cat_(x<-s|P x)f x -> exists x : X, x \in s /\ y \in f x
y: Y
CONS: y \in \cat_(j<-s|P j)f j
x: X
INs: x \in s
INfx: y \in f x
exists x : X, x \in a :: s /\ y \in f x
      exists x; split =>//.
X, Y: eqType
f: X -> seq Y
P: X -> bool
a: X
s: seq X
IHs: forall y : Y, y \in \cat_(x<-s|P x)f x -> exists x : X, x \in s /\ y \in f x
y: Y
CONS: y \in \cat_(j<-s|P j)f j
x: X
INs: x \in s
INfx: y \in f x
x \in a :: s
      by rewrite in_cons; apply /orP; right.
  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 :
    forall xss P, 
      [seq x <- \cat_(xs <- xss) f xs | P x]  =        
      \cat_(xs <- xss) [seq x <- f xs | P x] .
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.
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]
    move=> xss P.
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]
    elim: xss => [|a xss IHxss].
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]
X, Y: eqType
f: X -> seq Y
P: Y -> bool
a: X
xss: seq X
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]
    -
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] by rewrite !big_nil.
    -
X, Y: eqType
f: X -> seq Y
P: Y -> bool
a: X
xss: seq X
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.
  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.

    (** Consider a list [xs], ... *)
    Context {xs : seq X}.

    (** ... a filter predicate [P], ... *)
    Context {P : pred X}.

    (** ... assume that there are no duplicates in each of the possible
        sequences to concatenate... *)
    Hypothesis H_uniq_f : forall x, P x -> uniq (f x).
    
    (** ...and that there are no elements in common between the sequences. *)
    Hypothesis H_no_elements_in_common :
      forall 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 :
        uniq xs ->
        uniq (\cat_(x <- xs | P x) (f x)).
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P 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
uniq xs -> uniq (\cat_(x<-xs|P x)f x)
    Proof.
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P 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
uniq xs -> uniq (\cat_(x<-xs|P x)f x)
      move: xs.
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P 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|P x)f x)
      elim=> [|a xs' IHxs]; first by rewrite big_nil.
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P 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'|P x)f x)
uniq (a :: xs') -> uniq (\cat_(x<-(a :: xs')|P x)f x)
      rewrite cons_uniq => /andP [NINxs UNIQ].
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P 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'|P x)f x)
NINxs: a \notin xs'
UNIQ: uniq xs'
uniq (\cat_(x<-(a :: xs')|P x)f x)
      rewrite big_cons.
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P 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'|P x)f x)
NINxs: a \notin xs'
UNIQ: uniq xs'
uniq
  (if P a
   then f a ++ \cat_(j<-xs'|P j)f j
   else \cat_(j<-xs'|P j)f j)
      case Pa: (P a) => //.
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P 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'|P x)f x)
NINxs: a \notin xs'
UNIQ: uniq xs'
Pa: P a = true
uniq (f a ++ \cat_(j<-xs'|P j)f j)
      rewrite cat_uniq.
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P 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'|P x)f x)
NINxs: a \notin xs'
UNIQ: uniq xs'
Pa: P a = true
[&& uniq (f a), ~~ has [in f a] (\cat_(j<-xs'|P j)f j)
  & uniq (\cat_(j<-xs'|P j)f j)]
      apply /andP; split; first by apply H_uniq_f.
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P 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'|P x)f x)
NINxs: a \notin xs'
UNIQ: uniq xs'
Pa: P a = true
~~ has [in f a] (\cat_(j<-xs'|P j)f j) &&
uniq (\cat_(j<-xs'|P j)f j)
      apply /andP; split; last by apply IHxs.
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P 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'|P x)f x)
NINxs: a \notin xs'
UNIQ: uniq xs'
Pa: P a = true
~~ has [in f a] (\cat_(j<-xs'|P j)f j)
      apply /hasPn=> x IN; apply /negP=> INfa.
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P 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'|P x)f x)
NINxs: a \notin xs'
UNIQ: uniq xs'
Pa: P a = true
x: Y
IN: x \in \cat_(j<-xs'|P j)f j
INfa: x \in f a
False
      move: (mem_bigcat_exists _ _ IN) => [a' [INxs INfa']].
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P 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'|P x)f x)
NINxs: a \notin xs'
UNIQ: uniq xs'
Pa: P a = true
x: Y
IN: x \in \cat_(j<-xs'|P j)f j
INfa: x \in f a
a': X
INxs: a' \in xs'
INfa': x \in f a'
False
      move: (H_no_elements_in_common x a a' INfa INfa') => EQa.
X, Y: eqType
f: X -> seq Y
xs: seq X
P: pred X
H_uniq_f: forall x : X, P 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'|P x)f x)
NINxs: a \notin xs'
UNIQ: uniq xs'
Pa: P a = true
x: Y
IN: x \in \cat_(j<-xs'|P j)f j
INfa: x \in f a
a': X
INxs: a' \in xs'
INfa': x \in f a'
EQa: a = a'
False
      by move: NINxs; rewrite EQa => /negP CONTRA.
    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 : forall 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 :
      forall x1 x2,
        x1 != x2 ->
        [seq x <- f x1 | g x == x2] = [::].
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.
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] = [::]
      move => x1 x2 => /negP NEQ.
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.
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.
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.
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.
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.
    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 :
      forall y xs,
        y \in xs ->
        uniq xs -> 
        \cat_(x <- xs) [seq x' <- f x | g x' == y] = f y.
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.
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
      move=> y xs IN UNI.
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
      elim: xs IN UNI => [//|x' xs IHxs] IN UNI.
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
IHxs: y \in xs ->
uniq xs ->
\cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
IN: y \in x' :: xs
UNI: uniq (x' :: xs)
\cat_(x<-(x' :: xs))[seq x' <- f x | g x' == y] = f y
      move: IN; rewrite in_cons => /orP [/eqP EQ| IN].
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
IHxs: y \in xs ->
uniq xs ->
\cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
UNI: uniq (x' :: xs)
EQ: y = x'
\cat_(x<-(x' :: xs))[seq x' <- f x | g x' == y] = f y
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
IHxs: y \in xs ->
uniq xs ->
\cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
UNI: uniq (x' :: xs)
IN: y \in xs
\cat_(x<-(x' :: xs))[seq x' <- f x | g x' == y] = f y
      {
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
IHxs: y \in xs ->
uniq xs ->
\cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
UNI: uniq (x' :: xs)
EQ: y = x'
\cat_(x<-(x' :: xs))[seq x' <- f x | g x' == y] = f y subst; rewrite !big_cons.
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
IHxs: x' \in xs ->
uniq xs ->
\cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] =
f x'
UNI: uniq (x' :: xs)
[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'.
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
IHxs: x' \in xs ->
uniq xs ->
\cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] =
f x'
UNI: uniq (x' :: xs)
[seq x <- f x' | g x == x'] = f x'
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
IHxs: x' \in xs ->
uniq xs ->
\cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] =
f x'
UNI: uniq (x' :: xs)
f x' ++ \cat_(j<-xs)[seq x'0 <- f j | g x'0 == x'] =
f x'
        {
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
IHxs: x' \in xs ->
uniq xs ->
\cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] =
f x'
UNI: uniq (x' :: xs)
[seq x <- f x' | g x == x'] = f x' apply/all_filterP/allP.
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
IHxs: x' \in xs ->
uniq xs ->
\cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] =
f x'
UNI: uniq (x' :: xs)
{in f x', forall x : Y, g x == x'}
          intros y IN; apply/eqP.
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
IHxs: x' \in xs ->
uniq xs ->
\cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] =
f x'
UNI: uniq (x' :: xs)
y: Y
IN: y \in f x'
g y = x'
          by apply H_g_cancels_f. }
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
IHxs: x' \in xs ->
uniq xs ->
\cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] =
f x'
UNI: uniq (x' :: xs)
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.
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
IHxs: x' \in xs ->
uniq xs ->
\cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] =
f x'
UNI: uniq (x' :: xs)
\cat_(j<-xs)[seq x <- f j | g x == x'] = [::]
        rewrite big1_seq //; move => xs2 /andP [_ IN].
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
IHxs: x' \in xs ->
uniq xs ->
\cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] =
f x'
UNI: uniq (x' :: xs)
xs2: X
IN: xs2 \in xs
[seq x <- f xs2 | g x == x'] = [::]
        have NEQ: xs2 != x'; last by rewrite seq_different_elements_nil.
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
IHxs: x' \in xs ->
uniq xs ->
\cat_(x<-xs)[seq x'0 <- f x | g x'0 == x'] =
f x'
UNI: uniq (x' :: xs)
xs2: X
IN: xs2 \in xs
xs2 != x'
        apply/neqP; intros EQ; subst x'.
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
UNI: uniq (xs2 :: xs)
IHxs: xs2 \in xs ->
uniq xs ->
\cat_(x<-xs)[seq x' <- f x | g x' == xs2] =
f xs2
IN: xs2 \in xs
False
        move: UNI; rewrite cons_uniq => /andP [NIN _].
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. }
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
IHxs: y \in xs ->
uniq xs ->
\cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
UNI: uniq (x' :: xs)
IN: y \in xs
\cat_(x<-(x' :: xs))[seq x' <- f x | g x' == y] = f y
      {
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
IHxs: y \in xs ->
uniq xs ->
\cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
UNI: uniq (x' :: xs)
IN: y \in xs
\cat_(x<-(x' :: xs))[seq x' <- f x | g x' == y] = f y rewrite big_cons IHxs //; last by move:UNI; rewrite cons_uniq=> /andP[_ ?].
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
IHxs: y \in xs ->
uniq xs ->
\cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
UNI: uniq (x' :: xs)
IN: y \in xs
[seq x' <- f x' | g x' == y] ++ f y = f y
        have NEQ: (x' != y); last by rewrite seq_different_elements_nil.
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
IHxs: y \in xs ->
uniq xs ->
\cat_(x<-xs)[seq x' <- f x | g x' == y] = f y
UNI: uniq (x' :: xs)
IN: y \in xs
x' != y
        apply/neqP; intros EQ; subst x'.
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
UNI: uniq (y :: xs)
IN: y \in xs
False
        move: UNI; rewrite cons_uniq => /andP [NIN _].
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. }
    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 :
    forall xs ys,
      count P (\cat_(x <- xs) \cat_(y <- ys) F x y) =
      count P (\cat_(y <- ys) \cat_(x <- xs) F x y).
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.
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)
    elim=> [|x0 seqX IHxs]; elim=> [|y0 seqY IHys].
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)
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)
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)
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)
    {
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. }
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)
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)
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)
    {
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. }
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)
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) 
    {
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. }
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) 
    {
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.
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.
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.
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.
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. } 
  Qed.

End BigCatNestedCount.

(** In the following section we introduce a lemma that relates to partitioning.*)
Section BigCatPartitionLemma.
  (** Consider an item type [X] and partition type [Y] both supporting equality comparisons. *)
  Variable X Y : eqType.

  (** Consider a sequence of items of type [X] ... *)
  Variable xs : seq X.
  (** ... and a sequence of partitions. *)
  Variable ys : seq Y.

  (** Consider a predicate [P] on [X]. *)
  Variable P : pred X.

  (** Define a mapping from items to partitions. *)
  Variable x_to_y : X -> Y.

  (** We assume that any item in [xs] has its corresponding partition in the sequence of partitions [ys]. *)
  Hypothesis H_no_partition_missing : forall x, x \in xs -> P x -> x_to_y x \in ys.

  (** Consider a partition of [xs]. *)
  Let partitioned_seq (y : Y) := [seq x <- xs | P x && (x_to_y x == y)].

  (** We prove that any element in [xs] is also contained in the union of the partitions. *)
  Lemma bigcat_partitions:
    forall j,
      (j \in [seq x <- xs | P x])
      = (j \in \cat_(y <- ys) partitioned_seq y).
X, Y: eqType
xs: seq X
ys: seq Y
P: pred X
x_to_y: X -> Y
H_no_partition_missing: forall x : X,
x \in xs ->
P x -> x_to_y x \in ys
partitioned_seq:= fun y : Y =>
[seq x <- xs | P x & x_to_y x == y]: Y -> seq X
forall j : X,
(j \in [seq x <- xs | P x]) =
(j \in \cat_(y<-ys)partitioned_seq y)
  Proof.
X, Y: eqType
xs: seq X
ys: seq Y
P: pred X
x_to_y: X -> Y
H_no_partition_missing: forall x : X,
x \in xs ->
P x -> x_to_y x \in ys
partitioned_seq:= fun y : Y =>
[seq x <- xs | P x & x_to_y x == y]: Y -> seq X
forall j : X,
(j \in [seq x <- xs | P x]) =
(j \in \cat_(y<-ys)partitioned_seq y)
    move=> j.
X, Y: eqType
xs: seq X
ys: seq Y
P: pred X
x_to_y: X -> Y
H_no_partition_missing: forall x : X,
x \in xs ->
P x -> x_to_y x \in ys
partitioned_seq:= fun y : Y =>
[seq x <- xs | P x & x_to_y x == y]: Y -> seq X
j: X
(j \in [seq x <- xs | P x]) =
(j \in \cat_(y<-ys)partitioned_seq y)
    apply /idP/idP.
X, Y: eqType
xs: seq X
ys: seq Y
P: pred X
x_to_y: X -> Y
H_no_partition_missing: forall x : X,
x \in xs ->
P x -> x_to_y x \in ys
partitioned_seq:= fun y : Y =>
[seq x <- xs | P x & x_to_y x == y]: Y -> seq X
j: X
j \in [seq x <- xs | P x] ->
j \in \cat_(y<-ys)partitioned_seq y
X, Y: eqType
xs: seq X
ys: seq Y
P: pred X
x_to_y: X -> Y
H_no_partition_missing: forall x : X,
x \in xs ->
P x -> x_to_y x \in ys
partitioned_seq:= fun y : Y =>
[seq x <- xs | P x & x_to_y x == y]: Y -> seq X
j: X
j \in \cat_(y<-ys)partitioned_seq y ->
j \in [seq x <- xs | P x]
    {
X, Y: eqType
xs: seq X
ys: seq Y
P: pred X
x_to_y: X -> Y
H_no_partition_missing: forall x : X,
x \in xs ->
P x -> x_to_y x \in ys
partitioned_seq:= fun y : Y =>
[seq x <- xs | P x & x_to_y x == y]: Y -> seq X
j: X
j \in [seq x <- xs | P x] ->
j \in \cat_(y<-ys)partitioned_seq y rewrite mem_filter => /andP [PredJ_true IN].
X, Y: eqType
xs: seq X
ys: seq Y
P: pred X
x_to_y: X -> Y
H_no_partition_missing: forall x : X,
x \in xs ->
P x -> x_to_y x \in ys
partitioned_seq:= fun y : Y =>
[seq x <- xs | P x & x_to_y x == y]: Y -> seq X
j: X
PredJ_true: P j
IN: j \in xs
j \in \cat_(y<-ys)partitioned_seq y
      apply mem_bigcat with (x := x_to_y j).
X, Y: eqType
xs: seq X
ys: seq Y
P: pred X
x_to_y: X -> Y
H_no_partition_missing: forall x : X,
x \in xs ->
P x -> x_to_y x \in ys
partitioned_seq:= fun y : Y =>
[seq x <- xs | P x & x_to_y x == y]: Y -> seq X
j: X
PredJ_true: P j
IN: j \in xs
x_to_y j \in ys
X, Y: eqType
xs: seq X
ys: seq Y
P: pred X
x_to_y: X -> Y
H_no_partition_missing: forall x : X,
x \in xs ->
P x -> x_to_y x \in ys
partitioned_seq:= fun y : Y =>
[seq x <- xs | P x & x_to_y x == y]: Y -> seq X
j: X
PredJ_true: P j
IN: j \in xs
j \in partitioned_seq (x_to_y j)
      {
X, Y: eqType
xs: seq X
ys: seq Y
P: pred X
x_to_y: X -> Y
H_no_partition_missing: forall x : X,
x \in xs ->
P x -> x_to_y x \in ys
partitioned_seq:= fun y : Y =>
[seq x <- xs | P x & x_to_y x == y]: Y -> seq X
j: X
PredJ_true: P j
IN: j \in xs
x_to_y j \in ys move: IN PredJ_true.
X, Y: eqType
xs: seq X
ys: seq Y
P: pred X
x_to_y: X -> Y
H_no_partition_missing: forall x : X,
x \in xs ->
P x -> x_to_y x \in ys
partitioned_seq:= fun y : Y =>
[seq x <- xs | P x & x_to_y x == y]: Y -> seq X
j: X
j \in xs -> P j -> x_to_y j \in ys
        by apply H_no_partition_missing. }
X, Y: eqType
xs: seq X
ys: seq Y
P: pred X
x_to_y: X -> Y
H_no_partition_missing: forall x : X,
x \in xs ->
P x -> x_to_y x \in ys
partitioned_seq:= fun y : Y =>
[seq x <- xs | P x & x_to_y x == y]: Y -> seq X
j: X
PredJ_true: P j
IN: j \in xs
j \in partitioned_seq (x_to_y j)
      rewrite mem_filter.
X, Y: eqType
xs: seq X
ys: seq Y
P: pred X
x_to_y: X -> Y
H_no_partition_missing: forall x : X,
x \in xs ->
P x -> x_to_y x \in ys
partitioned_seq:= fun y : Y =>
[seq x <- xs | P x & x_to_y x == y]: Y -> seq X
j: X
PredJ_true: P j
IN: j \in xs
P j && (x_to_y j == x_to_y j) && (j \in xs)
      by do 2! [apply /andP; split; eauto]. }
X, Y: eqType
xs: seq X
ys: seq Y
P: pred X
x_to_y: X -> Y
H_no_partition_missing: forall x : X,
x \in xs ->
P x -> x_to_y x \in ys
partitioned_seq:= fun y : Y =>
[seq x <- xs | P x & x_to_y x == y]: Y -> seq X
j: X
j \in \cat_(y<-ys)partitioned_seq y ->
j \in [seq x <- xs | P x]
    {
X, Y: eqType
xs: seq X
ys: seq Y
P: pred X
x_to_y: X -> Y
H_no_partition_missing: forall x : X,
x \in xs ->
P x -> x_to_y x \in ys
partitioned_seq:= fun y : Y =>
[seq x <- xs | P x & x_to_y x == y]: Y -> seq X
j: X
j \in \cat_(y<-ys)partitioned_seq y ->
j \in [seq x <- xs | P x] move=> /mem_bigcat_exists [x [x_IN IN]].
X, Y: eqType
xs: seq X
ys: seq Y
P: pred X
x_to_y: X -> Y
H_no_partition_missing: forall x : X,
x \in xs ->
P x -> x_to_y x \in ys
partitioned_seq:= fun y : Y =>
[seq x <- xs | P x & x_to_y x == y]: Y -> seq X
j: X
x: Y
x_IN: x \in ys
IN: j \in partitioned_seq x
j \in [seq x <- xs | P x]
      move: IN.
X, Y: eqType
xs: seq X
ys: seq Y
P: pred X
x_to_y: X -> Y
H_no_partition_missing: forall x : X,
x \in xs ->
P x -> x_to_y x \in ys
partitioned_seq:= fun y : Y =>
[seq x <- xs | P x & x_to_y x == y]: Y -> seq X
j: X
x: Y
x_IN: x \in ys
j \in partitioned_seq x -> j \in [seq x <- xs | P x]
      rewrite !mem_filter.
X, Y: eqType
xs: seq X
ys: seq Y
P: pred X
x_to_y: X -> Y
H_no_partition_missing: forall x : X,
x \in xs ->
P x -> x_to_y x \in ys
partitioned_seq:= fun y : Y =>
[seq x <- xs | P x & x_to_y x == y]: Y -> seq X
j: X
x: Y
x_IN: x \in ys
P j && (x_to_y j == x) && (j \in xs) ->
P j && (j \in xs)
      move=> /andP [/andP [PredJ X_to_Y_eq] IN].
X, Y: eqType
xs: seq X
ys: seq Y
P: pred X
x_to_y: X -> Y
H_no_partition_missing: forall x : X,
x \in xs ->
P x -> x_to_y x \in ys
partitioned_seq:= fun y : Y =>
[seq x <- xs | P x & x_to_y x == y]: Y -> seq X
j: X
x: Y
x_IN: x \in ys
PredJ: P j
X_to_Y_eq: x_to_y j == x
IN: j \in xs
P j && (j \in xs)
      by apply /andP. }
  Qed.

End BigCatPartitionLemma.