From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]

Require Export prosa.util.notation.
Require Export prosa.util.rel.
Require Export prosa.util.nat.

Section SumsOverSequences.

  (** Consider any type [I] with a decidable equality ... *)
  Variable (I : eqType).

  (** ... and assume we are given a sequence ... *)
  Variable (r : seq I).

  (** ... and a predicate [P]. *)
  Variable (P : pred I).

  (** First, we will show some properties of the sum performed over a single function
      yielding natural numbers. *)
  Section SumOfOneFunction.

    (** Consider any function that yields natural numbers. *)
    Variable (F : I -> nat).

    (** We start showing that having every member of [r] equal to zero is equivalent to
        having the sum of all the elements of [r] equal to zero, and vice-versa. *)
    Lemma sum_nat_eq0_nat :
      (\sum_(i <- r | P i) F i == 0) = all (fun x => F x == 0) [seq x <- r | P x].
I: eqType
r: seq I
P: pred I
F: I -> nat
(\sum_(i <- r | P i) F i == 0) =
all (fun x : I => F x == 0) [seq x <- r | P x]
    Proof.
I: eqType
r: seq I
P: pred I
F: I -> nat
(\sum_(i <- r | P i) F i == 0) =
all (fun x : I => F x == 0) [seq x <- r | P x]
      elim: r => [|x r' IH]; rewrite ?big_nil//= big_cons.
I: eqType
r: seq I
P: pred I
F: I -> nat
x: I
r': seq I
IH: (\sum_(i <- r' | P i) F i == 0) =
all (fun x : I => F x == 0) [seq x <- r' | P x]
((if P x
  then F x + \sum_(j <- r' | P j) F j
  else \sum_(j <- r' | P j) F j) == 0) =
all (fun x : I => F x == 0)
  (if P x
   then x :: [seq x <- r' | P x]
   else [seq x <- r' | P x])
      by case: ifP; rewrite ?addn_eq0 IH.
    Qed.

    (** In the same way, if at least one element of [r] is not zero, then the sum of all
        elements of [r] must be strictly positive, and vice-versa. *)
    Lemma sum_nat_gt0 :
      (0 < \sum_(i <- r | P i) F i) = has (fun x => 0 < F x) [seq x <- r | P x].
I: eqType
r: seq I
P: pred I
F: I -> nat
(0 < \sum_(i <- r | P i) F i) =
has (fun x : I => 0 < F x) [seq x <- r | P x]
    Proof.
I: eqType
r: seq I
P: pred I
F: I -> nat
(0 < \sum_(i <- r | P i) F i) =
has (fun x : I => 0 < F x) [seq x <- r | P x]
      apply/negb_inj; rewrite lt0n negbK sum_nat_eq0_nat -all_predC.
I: eqType
r: seq I
P: pred I
F: I -> nat
all (fun x : I => F x == 0) [seq x <- r | P x] =
all (predC (fun x : I => 0 < F x)) [seq x <- r | P x]
      by apply/eq_all => ?; rewrite /= lt0n negbK.
    Qed.

    (** Next, we show that if a number [a] is not contained in [r], then filtering or not
        filtering [a] when summing leads to the same result. *)
    Lemma sum_notin_rem_eqn a :
      a \notin r ->
      \sum_(x <- r | P x && (x != a)) F x = \sum_(x <- r | P x) F x.
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
a \notin r ->
\sum_(x <- r | P x && (x != a)) F x =
\sum_(x <- r | P x) F x
    Proof.
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
a \notin r ->
\sum_(x <- r | P x && (x != a)) F x =
\sum_(x <- r | P x) F x
      move=> a_notin_r; rewrite [LHS]big_seq_cond [RHS]big_seq_cond.
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
a_notin_r: a \notin r
\sum_(i <- r | [&& i \in r, P i & i != a]) F i =
\sum_(i <- r | (i \in r) && P i) F i
      apply: eq_bigl => x; case xinr: (x \in r) => //=.
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
a_notin_r: a \notin r
x: I
xinr: (x \in r) = true
P x && (x != a) = P x
      have [xa|] := eqP; last by rewrite andbT.
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
a_notin_r: a \notin r
x: I
xinr: (x \in r) = true
xa: x = a
P x && ~~ true = P x
      by move: xinr a_notin_r; rewrite xa => ->.
    Qed.

    (** We prove that if any element of [r] is bounded by constant [c],
        then the sum of the whole set is bounded by [c * size r]. *)
    Lemma sum_majorant_constant c :
      (forall a, a \in r -> P a -> F a <= c) ->
      \sum_(j <- r | P j) F j <= c * (size [seq j <- r | P j]).
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
(forall a : I, a \in r -> P a -> F a <= c) ->
\sum_(j <- r | P j) F j <= c * size [seq j <- r | P j]
    Proof.
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
(forall a : I, a \in r -> P a -> F a <= c) ->
\sum_(j <- r | P j) F j <= c * size [seq j <- r | P j]
      move=> Fa_le_c.
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
Fa_le_c: forall a : I, a \in r -> P a -> F a <= c
\sum_(j <- r | P j) F j <= c * size [seq j <- r | P j]
      rewrite -sum1_size big_filter big_distrr/= muln1.
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
Fa_le_c: forall a : I, a \in r -> P a -> F a <= c
\sum_(j <- r | P j) F j <= \sum_(i <- r | P i) c
      rewrite big_seq_cond [X in _ <= X]big_seq_cond.
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
Fa_le_c: forall a : I, a \in r -> P a -> F a <= c
\sum_(i <- r | (i \in r) && P i) F i <=
\sum_(i <- r | (i \in r) && P i) c
      apply: leq_sum => i /andP[ir Pi]; exact: Fa_le_c.
    Qed.

    (** Next, we show that the sum of the elements in [r] respecting [P] can
        be obtained by removing from the total sum over [r] the sum of the elements
        in [r] not respecting [P]. *)
    Lemma sum_pred_diff:
      \sum_(r <- r | P r) F r = \sum_(r <- r) F r - \sum_(r <- r | ~~ P r) F r.
I: eqType
r: seq I
P: pred I
F: I -> nat
\sum_(r <- r | P r) F r =
\sum_(r <- r) F r - \sum_(r <- r | ~~ P r) F r
    Proof.
I: eqType
r: seq I
P: pred I
F: I -> nat
\sum_(r <- r | P r) F r =
\sum_(r <- r) F r - \sum_(r <- r | ~~ P r) F r by rewrite [X in X - _](bigID P)/= addnK. Qed.

  End SumOfOneFunction.

  (** In this section, we show some properties of the sum performed over two different functions. *)
  Section SumOfTwoFunctions.

    (** Consider three functions that yield natural numbers. *)
    Variable (E E1 E2 : I -> nat).

    (** Besides earlier introduced predicate [P], we add two additional predicates [P1] and [P2]. *)
    Variable (P1 P2 : pred I).

    (** Assume that [E2] dominates [E1] in all the points contained in the set [r] and respecting
        the predicate [P]. We prove that, if we sum both function over those points, then the sum
        of [E2] will dominate the sum of [E1]. *)
    Lemma leq_sum_seq :
      (forall i, i \in r -> P i -> E1 i <= E2 i) ->
      \sum_(i <- r | P i) E1 i <= \sum_(i <- r | P i) E2 i.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
(forall i : I, i \in r -> P i -> E1 i <= E2 i) ->
\sum_(i <- r | P i) E1 i <= \sum_(i <- r | P i) E2 i
    Proof.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
(forall i : I, i \in r -> P i -> E1 i <= E2 i) ->
\sum_(i <- r | P i) E1 i <= \sum_(i <- r | P i) E2 i
      move=> le; rewrite big_seq_cond [X in _ <= X]big_seq_cond.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
le: forall i : I, i \in r -> P i -> E1 i <= E2 i
\sum_(i <- r | (i \in r) && P i) E1 i <=
\sum_(i <- r | (i \in r) && P i) E2 i
      apply: leq_sum => i /andP[]; exact: le.
    Qed.

    (** In the same way, if [E1] equals [E2] in all the points considered above, then also the two
        sums will be identical. *)
    Lemma eq_sum_seq:
      (forall i, i \in r -> P i -> E1 i == E2 i) ->
      \sum_(i <- r | P i) E1 i == \sum_(i <- r | P i) E2 i.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
(forall i : I, i \in r -> P i -> E1 i == E2 i) ->
\sum_(i <- r | P i) E1 i == \sum_(i <- r | P i) E2 i
    Proof.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
(forall i : I, i \in r -> P i -> E1 i == E2 i) ->
\sum_(i <- r | P i) E1 i == \sum_(i <- r | P i) E2 i
      move=> eqE; apply/eqP; rewrite -big_filter -[RHS]big_filter.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
eqE: forall i : I, i \in r -> P i -> E1 i == E2 i
\sum_(i <- [seq x <- r | P x]) E1 i =
\sum_(i <- [seq x <- r | P x]) E2 i
      apply: eq_big_seq => x; rewrite mem_filter => /andP[Px xr]; exact/eqP/eqE.
    Qed.

    (** Assume that [P1] implies [P2] in all the points contained in
        the set [r]. We prove that, if we sum both functions over those
        points, then the sum of [E] conditioned by [P2] will dominate
        the sum of [E] conditioned by [P1]. *)
    Lemma leq_sum_seq_pred:
      (forall i, i \in r -> P1 i -> P2 i) ->
      \sum_(i <- r | P1 i) E i <= \sum_(i <- r | P2 i) E i.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
(forall i : I, i \in r -> P1 i -> P2 i) ->
\sum_(i <- r | P1 i) E i <= \sum_(i <- r | P2 i) E i
    Proof.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
(forall i : I, i \in r -> P1 i -> P2 i) ->
\sum_(i <- r | P1 i) E i <= \sum_(i <- r | P2 i) E i
      move=> imp; rewrite [X in _ <= X](bigID P1)/=.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
imp: forall i : I, i \in r -> P1 i -> P2 i
\sum_(i <- r | P1 i) E i <=
\sum_(i <- r | P2 i && P1 i) E i +
\sum_(i <- r | P2 i && ~~ P1 i) E i
      rewrite big_seq_cond [X in _ <= X + _]big_seq_cond.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
imp: forall i : I, i \in r -> P1 i -> P2 i
\sum_(i <- r | (i \in r) && P1 i) E i <=
\sum_(i <- r | [&& i \in r, P2 i & P1 i]) E i +
\sum_(i <- r | P2 i && ~~ P1 i) E i
      rewrite (eq_bigl (fun i => [&& i \in r, P2 i & P1 i])) ?leq_addr// => i.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
imp: forall i : I, i \in r -> P1 i -> P2 i
i: I
(i \in r) && P1 i = [&& i \in r, P2 i & P1 i]
      by case ir: (i \in r); case P1i: (P1 i); rewrite ?andbF //= (imp i).
    Qed.

  End SumOfTwoFunctions.

End SumsOverSequences.

(** For technical (and temporary) reasons related to the proof style, the next
    two lemmas are stated outside of the section, but conceptually make use of a
    similar context.

    First, we observe that summing over a subset of a given sequence, if all
    summands are natural numbers, cannot yield a larger sum. *)
Lemma leq_sum_subseq (I : eqType) (r r' : seq I) (P : pred I) (F : I -> nat) :
  subseq r r' ->
  \sum_(i <- r | P i) F i <= \sum_(i <- r' | P i) F i.
I: eqType
r, r': seq I
P: pred I
F: I -> nat
subseq r r' ->
\sum_(i <- r | P i) F i <= \sum_(i <- r' | P i) F i
Proof.
I: eqType
r, r': seq I
P: pred I
F: I -> nat
subseq r r' ->
\sum_(i <- r | P i) F i <= \sum_(i <- r' | P i) F i
  elim: r r' => [|x r IH] r'; first by rewrite big_nil.
I: eqType
P: pred I
F: I -> nat
x: I
r: seq I
IH: forall r' : seq I,
subseq r r' ->
\sum_(i <- r | P i) F i <=
\sum_(i <- r' | P i) F i
r': seq I
subseq (x :: r) r' ->
\sum_(i <- (x :: r) | P i) F i <=
\sum_(i <- r' | P i) F i
  elim: r' => [//|x' r' IH'] /=; have [<- /IH {}IH|_ /IH' {}IH'] := eqP.
I: eqType
P: pred I
F: I -> nat
x: I
r: seq I
x': I
r': seq I
IH': subseq (x :: r) r' ->
\sum_(i <- (x :: r) | P i) F i <= \sum_(i <- r' | P i) F i
IH: \sum_(i <- r | P i) F i <=
\sum_(i <- r' | P i) F i
\sum_(i <- (x :: r) | P i) F i <=
\sum_(i <- (x :: r') | P i) F i
I: eqType
P: pred I
F: I -> nat
x: I
r: seq I
IH: forall r' : seq I,
subseq r r' ->
\sum_(i <- r | P i) F i <=
\sum_(i <- r' | P i) F i
x': I
r': seq I
IH': \sum_(i <- (x :: r) | P i) F i <= \sum_(i <- r' | P i) F i
\sum_(i <- (x :: r) | P i) F i <=
\sum_(i <- (x' :: r') | P i) F i
  -
I: eqType
P: pred I
F: I -> nat
x: I
r: seq I
x': I
r': seq I
IH': subseq (x :: r) r' ->
\sum_(i <- (x :: r) | P i) F i <= \sum_(i <- r' | P i) F i
IH: \sum_(i <- r | P i) F i <=
\sum_(i <- r' | P i) F i
\sum_(i <- (x :: r) | P i) F i <=
\sum_(i <- (x :: r') | P i) F i
I: eqType
P: pred I
F: I -> nat
x: I
r: seq I
IH: forall r' : seq I,
subseq r r' ->
\sum_(i <- r | P i) F i <=
\sum_(i <- r' | P i) F i
x': I
r': seq I
IH': \sum_(i <- (x :: r) | P i) F i <= \sum_(i <- r' | P i) F i
\sum_(i <- (x :: r) | P i) F i <=
\sum_(i <- (x' :: r') | P i) F i by rewrite !big_cons; case: (P x); rewrite // leq_add2l.
I: eqType
P: pred I
F: I -> nat
x: I
r: seq I
IH: forall r' : seq I,
subseq r r' ->
\sum_(i <- r | P i) F i <=
\sum_(i <- r' | P i) F i
x': I
r': seq I
IH': \sum_(i <- (x :: r) | P i) F i <= \sum_(i <- r' | P i) F i
\sum_(i <- (x :: r) | P i) F i <=
\sum_(i <- (x' :: r') | P i) F i
  -
I: eqType
P: pred I
F: I -> nat
x: I
r: seq I
IH: forall r' : seq I,
subseq r r' ->
\sum_(i <- r | P i) F i <=
\sum_(i <- r' | P i) F i
x': I
r': seq I
IH': \sum_(i <- (x :: r) | P i) F i <= \sum_(i <- r' | P i) F i
\sum_(i <- (x :: r) | P i) F i <=
\sum_(i <- (x' :: r') | P i) F i rewrite [X in _ <= X]big_cons; case: (P x') => //.
I: eqType
P: pred I
F: I -> nat
x: I
r: seq I
IH: forall r' : seq I,
subseq r r' ->
\sum_(i <- r | P i) F i <=
\sum_(i <- r' | P i) F i
x': I
r': seq I
IH': \sum_(i <- (x :: r) | P i) F i <= \sum_(i <- r' | P i) F i
\sum_(i <- (x :: r) | P i) F i <=
F x' + \sum_(j <- r' | P j) F j
    exact: leq_trans (leq_addl _ _).
Qed.

(** Second, we repeat the above observation that summing a superset of natural
    numbers cannot yield a lesser sum, but phrase the claim differently.

    Requiring the absence of duplicate in [r] is a simple way to guarantee that
    the set inclusion [r <= rs] implies the actually required multiset
    inclusion. *)
Lemma leq_sum_sub_uniq (I : eqType) (r : seq I) (F : I -> nat) (rs : seq I) :
  uniq r -> {subset r <= rs} ->
  \sum_(i <- r) F i <= \sum_(i <- rs) F i.
I: eqType
r: seq I
F: I -> nat
rs: seq I
uniq r ->
{subset r <= rs} ->
\sum_(i <- r) F i <= \sum_(i <- rs) F i
Proof.
I: eqType
r: seq I
F: I -> nat
rs: seq I
uniq r ->
{subset r <= rs} ->
\sum_(i <- r) F i <= \sum_(i <- rs) F i
  move=> uniq_r sub_r_rs.
I: eqType
r: seq I
F: I -> nat
rs: seq I
uniq_r: uniq r
sub_r_rs: {subset r <= rs}
\sum_(i <- r) F i <= \sum_(i <- rs) F i
  rewrite [X in _ <= X](bigID (fun x => x \in r))/=.
I: eqType
r: seq I
F: I -> nat
rs: seq I
uniq_r: uniq r
sub_r_rs: {subset r <= rs}
\sum_(i <- r) F i <=
\sum_(i <- rs | i \in r) F i +
\sum_(i <- rs | i \notin r) F i
  apply: leq_trans (leq_addr _ _).
I: eqType
r: seq I
F: I -> nat
rs: seq I
uniq_r: uniq r
sub_r_rs: {subset r <= rs}
\sum_(i <- r) F i <= \sum_(i <- rs | i \in r) F i
  rewrite (perm_big (undup [seq x <- rs | x \in r])).
I: eqType
r: seq I
F: I -> nat
rs: seq I
uniq_r: uniq r
sub_r_rs: {subset r <= rs}
\big[addn_comoid/0]_(i <- undup
                            [seq x <- rs | x \in r])
   F i <= \sum_(i <- rs | i \in r) F i
I: eqType
r: seq I
F: I -> nat
rs: seq I
uniq_r: uniq r
sub_r_rs: {subset r <= rs}
perm_eq r (undup [seq x <- rs | x \in r])
  -
I: eqType
r: seq I
F: I -> nat
rs: seq I
uniq_r: uniq r
sub_r_rs: {subset r <= rs}
\big[addn_comoid/0]_(i <- undup
                            [seq x <- rs | x \in r])
   F i <= \sum_(i <- rs | i \in r) F i
I: eqType
r: seq I
F: I -> nat
rs: seq I
uniq_r: uniq r
sub_r_rs: {subset r <= rs}
perm_eq r (undup [seq x <- rs | x \in r]) rewrite -filter_undup big_filter_cond/=.
I: eqType
r: seq I
F: I -> nat
rs: seq I
uniq_r: uniq r
sub_r_rs: {subset r <= rs}
\sum_(i <- undup rs | (i \in r) && true) F i <=
\sum_(i <- rs | i \in r) F i
I: eqType
r: seq I
F: I -> nat
rs: seq I
uniq_r: uniq r
sub_r_rs: {subset r <= rs}
perm_eq r (undup [seq x <- rs | x \in r])
    under eq_bigl => ? do rewrite andbT; exact/leq_sum_subseq/undup_subseq.
I: eqType
r: seq I
F: I -> nat
rs: seq I
uniq_r: uniq r
sub_r_rs: {subset r <= rs}
perm_eq r (undup [seq x <- rs | x \in r])
  -
I: eqType
r: seq I
F: I -> nat
rs: seq I
uniq_r: uniq r
sub_r_rs: {subset r <= rs}
perm_eq r (undup [seq x <- rs | x \in r]) apply: uniq_perm; rewrite ?undup_uniq// => x.
I: eqType
r: seq I
F: I -> nat
rs: seq I
uniq_r: uniq r
sub_r_rs: {subset r <= rs}
x: I
(x \in r) = (x \in undup [seq x <- rs | x \in r])
    rewrite mem_undup mem_filter.
I: eqType
r: seq I
F: I -> nat
rs: seq I
uniq_r: uniq r
sub_r_rs: {subset r <= rs}
x: I
(x \in r) = (x \in r) && (x \in rs)
    by case xinr: (x \in r); rewrite // (sub_r_rs _ xinr).
Qed.

(** We continue establishing properties of sums over sequences, but start a new
    section here because some of the below proofs depend lemmas in the preceding
    section in their full generality. *)
Section SumsOverSequences.

  (** Consider any type [I] with a decidable equality ... *)
  Variable (I : eqType).

  (** ... and assume we are given a sequence ... *)
  Variable (r : seq I).

  (** ... and a predicate [P]. *)
  Variable (P : pred I).

  (** Consider two functions that yield natural numbers. *)
  Variable (E1 E2 : I -> nat).

  (** First, as an auxiliary lemma, we observe that, if [E1 j] is less than [E2
      j] for some element [j] involved in a summation (filtered by [P]), then
      the corresponding totals are not equal. *)
  Lemma ltn_sum_leq_seq j :
    j \in r ->
    P j ->
    E1 j < E2 j ->
    (forall i, i \in r -> P i -> E1 i <= E2 i) ->
    \sum_(x <- r | P x) E1 x < \sum_(x <- r | P x) E2 x.
I: eqType
r: seq I
P: pred I
E1, E2: I -> nat
j: I
j \in r ->
P j ->
E1 j < E2 j ->
(forall i : I, i \in r -> P i -> E1 i <= E2 i) ->
\sum_(x <- r | P x) E1 x < \sum_(x <- r | P x) E2 x
  Proof.
I: eqType
r: seq I
P: pred I
E1, E2: I -> nat
j: I
j \in r ->
P j ->
E1 j < E2 j ->
(forall i : I, i \in r -> P i -> E1 i <= E2 i) ->
\sum_(x <- r | P x) E1 x < \sum_(x <- r | P x) E2 x
    move=> jr Pj ltj le.
I: eqType
r: seq I
P: pred I
E1, E2: I -> nat
j: I
jr: j \in r
Pj: P j
ltj: E1 j < E2 j
le: forall i : I, i \in r -> P i -> E1 i <= E2 i
\sum_(x <- r | P x) E1 x < \sum_(x <- r | P x) E2 x
    rewrite (big_rem j)// [X in _ < X](big_rem j)//= Pj -addSn leq_add//.
I: eqType
r: seq I
P: pred I
E1, E2: I -> nat
j: I
jr: j \in r
Pj: P j
ltj: E1 j < E2 j
le: forall i : I, i \in r -> P i -> E1 i <= E2 i
\sum_(y <- rem (T:=I) j r | P y) E1 y <=
\sum_(y <- rem (T:=I) j r | P y) E2 y
    apply: leq_sum_seq => i /mem_rem; exact: le.
  Qed.

  (** Next, we prove that if for any element i of a set [r] the following two
      statements hold (1) [E1 i] is less than or equal to [E2 i] and (2) the sum
      [E1 x_1, ..., E1 x_n] is equal to the sum of [E2 x_1, ..., E2 x_n], then
      [E1 x] is equal to [E2 x] for any element x of [xs]. *)
  Lemma eq_sum_leq_seq :
    (forall i, i \in r -> P i -> E1 i <= E2 i) ->
    \sum_(x <- r | P x) E1 x == \sum_(x <- r | P x) E2 x
      = all (fun x => E1 x == E2 x) [seq x <- r | P x].
I: eqType
r: seq I
P: pred I
E1, E2: I -> nat
(forall i : I, i \in r -> P i -> E1 i <= E2 i) ->
(\sum_(x <- r | P x) E1 x == \sum_(x <- r | P x) E2 x) =
all (fun x : I => E1 x == E2 x) [seq x <- r | P x]
  Proof.
I: eqType
r: seq I
P: pred I
E1, E2: I -> nat
(forall i : I, i \in r -> P i -> E1 i <= E2 i) ->
(\sum_(x <- r | P x) E1 x == \sum_(x <- r | P x) E2 x) =
all (fun x : I => E1 x == E2 x) [seq x <- r | P x]
    move=> le; rewrite all_filter; case aE: all.
I: eqType
r: seq I
P: pred I
E1, E2: I -> nat
le: forall i : I, i \in r -> P i -> E1 i <= E2 i
aE: all
  (SimplPred
     (fun i : I => P i ==> (E1 i == E2 i))) r =
true
(\sum_(x <- r | P x) E1 x == \sum_(x <- r | P x) E2 x) =
true
I: eqType
r: seq I
P: pred I
E1, E2: I -> nat
le: forall i : I, i \in r -> P i -> E1 i <= E2 i
aE: all
  (SimplPred
     (fun i : I => P i ==> (E1 i == E2 i))) r =
false
(\sum_(x <- r | P x) E1 x == \sum_(x <- r | P x) E2 x) =
false
    apply: eq_sum_seq => i ir Pi; move: aE => /allP/(_ i ir)/implyP; exact.
I: eqType
r: seq I
P: pred I
E1, E2: I -> nat
le: forall i : I, i \in r -> P i -> E1 i <= E2 i
aE: all
  (SimplPred
     (fun i : I => P i ==> (E1 i == E2 i))) r =
false
(\sum_(x <- r | P x) E1 x == \sum_(x <- r | P x) E2 x) =
false
    have [j /andP[jr Pj] ltj] : exists2 j, (j \in r) && P j & E1 j < E2 j.
I: eqType
r: seq I
P: pred I
E1, E2: I -> nat
le: forall i : I, i \in r -> P i -> E1 i <= E2 i
aE: all
  (SimplPred
     (fun i : I => P i ==> (E1 i == E2 i))) r =
false
exists2 j : I, (j \in r) && P j & E1 j < E2 j
I: eqType
r: seq I
P: pred I
E1, E2: I -> nat
le: forall i : I, i \in r -> P i -> E1 i <= E2 i
aE: all
  (SimplPred
     (fun i : I => P i ==> (E1 i == E2 i))) r =
false
j: I
jr: j \in r
Pj: P j
ltj: E1 j < E2 j
(\sum_(x <- r | P x) E1 x == \sum_(x <- r | P x) E2 x) =
false
    have /negbT := aE; rewrite -has_predC => /hasP[j jr /=].
I: eqType
r: seq I
P: pred I
E1, E2: I -> nat
le: forall i : I, i \in r -> P i -> E1 i <= E2 i
aE: all
  (SimplPred
     (fun i : I => P i ==> (E1 i == E2 i))) r =
false
j: I
jr: j \in r
~~ (P j ==> (E1 j == E2 j)) ->
exists2 j : I, (j \in r) && P j & E1 j < E2 j
I: eqType
r: seq I
P: pred I
E1, E2: I -> nat
le: forall i : I, i \in r -> P i -> E1 i <= E2 i
aE: all
  (SimplPred
     (fun i : I => P i ==> (E1 i == E2 i))) r =
false
j: I
jr: j \in r
Pj: P j
ltj: E1 j < E2 j
(\sum_(x <- r | P x) E1 x == \sum_(x <- r | P x) E2 x) =
false
    rewrite negb_imply => /andP[Pj neq].
I: eqType
r: seq I
P: pred I
E1, E2: I -> nat
le: forall i : I, i \in r -> P i -> E1 i <= E2 i
aE: all
  (SimplPred
     (fun i : I => P i ==> (E1 i == E2 i))) r =
false
j: I
jr: j \in r
Pj: P j
neq: E1 j != E2 j
exists2 j : I, (j \in r) && P j & E1 j < E2 j
I: eqType
r: seq I
P: pred I
E1, E2: I -> nat
le: forall i : I, i \in r -> P i -> E1 i <= E2 i
aE: all
  (SimplPred
     (fun i : I => P i ==> (E1 i == E2 i))) r =
false
j: I
jr: j \in r
Pj: P j
ltj: E1 j < E2 j
(\sum_(x <- r | P x) E1 x == \sum_(x <- r | P x) E2 x) =
false
    -
I: eqType
r: seq I
P: pred I
E1, E2: I -> nat
le: forall i : I, i \in r -> P i -> E1 i <= E2 i
aE: all
  (SimplPred
     (fun i : I => P i ==> (E1 i == E2 i))) r =
false
j: I
jr: j \in r
Pj: P j
neq: E1 j != E2 j
exists2 j : I, (j \in r) && P j & E1 j < E2 j
I: eqType
r: seq I
P: pred I
E1, E2: I -> nat
le: forall i : I, i \in r -> P i -> E1 i <= E2 i
aE: all
  (SimplPred
     (fun i : I => P i ==> (E1 i == E2 i))) r =
false
j: I
jr: j \in r
Pj: P j
ltj: E1 j < E2 j
(\sum_(x <- r | P x) E1 x == \sum_(x <- r | P x) E2 x) =
false by exists j; first exact/andP; rewrite ltn_neqAle neq le.
I: eqType
r: seq I
P: pred I
E1, E2: I -> nat
le: forall i : I, i \in r -> P i -> E1 i <= E2 i
aE: all
  (SimplPred
     (fun i : I => P i ==> (E1 i == E2 i))) r =
false
j: I
jr: j \in r
Pj: P j
ltj: E1 j < E2 j
(\sum_(x <- r | P x) E1 x == \sum_(x <- r | P x) E2 x) =
false
    -
I: eqType
r: seq I
P: pred I
E1, E2: I -> nat
le: forall i : I, i \in r -> P i -> E1 i <= E2 i
aE: all
  (SimplPred
     (fun i : I => P i ==> (E1 i == E2 i))) r =
false
j: I
jr: j \in r
Pj: P j
ltj: E1 j < E2 j
(\sum_(x <- r | P x) E1 x == \sum_(x <- r | P x) E2 x) =
false by apply/negbTE; rewrite neq_ltn (ltn_sum_leq_seq j).
  Qed.

End SumsOverSequences.

(** In this section, we prove a variety of properties of sums performed over ranges. *)
Section SumsOverRanges.

  (** First, we prove that the sum of Δ ones is equal to Δ     . *)
  Lemma sum_of_ones:
    forall t Δ,
      \sum_(t <= x < t + Δ) 1 = Δ.
forall t Δ : nat, \sum_(t <= x < t + Δ) 1 = Δ
  Proof.
forall t Δ : nat, \sum_(t <= x < t + Δ) 1 = Δ by move=> t Δ; rewrite big_const_nat iter_addn_0 mul1n addKn. Qed.

  (** Next, we show that a sum of natural numbers equals zero if and only
      if all terms are zero. *)
  Lemma big_nat_eq0 m n F:
    \sum_(m <= i < n) F i = 0 <-> (forall i, m <= i < n -> F i = 0).
m, n: nat
F: nat -> nat
\sum_(m <= i < n) F i = 0 <->
(forall i : nat, m <= i < n -> F i = 0)
  Proof.
m, n: nat
F: nat -> nat
\sum_(m <= i < n) F i = 0 <->
(forall i : nat, m <= i < n -> F i = 0)
    split.
m, n: nat
F: nat -> nat
\sum_(m <= i < n) F i = 0 ->
forall i : nat, m <= i < n -> F i = 0
m, n: nat
F: nat -> nat
(forall i : nat, m <= i < n -> F i = 0) ->
\sum_(m <= i < n) F i = 0
    -
m, n: nat
F: nat -> nat
\sum_(m <= i < n) F i = 0 ->
forall i : nat, m <= i < n -> F i = 0
m, n: nat
F: nat -> nat
(forall i : nat, m <= i < n -> F i = 0) ->
\sum_(m <= i < n) F i = 0 rewrite /index_iota => /eqP.
m, n: nat
F: nat -> nat
\sum_(i <- iota m (n - m)) F i == 0 ->
forall i : nat, m <= i < n -> F i = 0
m, n: nat
F: nat -> nat
(forall i : nat, m <= i < n -> F i = 0) ->
\sum_(m <= i < n) F i = 0
      rewrite sum_nat_eq0_nat filter_predT => /allP ZERO i.
m, n: nat
F: nat -> nat
ZERO: {in iota m (n - m),
  forall x : nat_eqType, F x == 0}
i: nat
m <= i < n -> F i = 0
m, n: nat
F: nat -> nat
(forall i : nat, m <= i < n -> F i = 0) ->
\sum_(m <= i < n) F i = 0
      rewrite -mem_index_iota /index_iota => IN.
m, n: nat
F: nat -> nat
ZERO: {in iota m (n - m),
  forall x : nat_eqType, F x == 0}
i: nat
IN: i \in iota m (n - m)
F i = 0
m, n: nat
F: nat -> nat
(forall i : nat, m <= i < n -> F i = 0) ->
\sum_(m <= i < n) F i = 0
      by apply/eqP; apply ZERO.
m, n: nat
F: nat -> nat
(forall i : nat, m <= i < n -> F i = 0) ->
\sum_(m <= i < n) F i = 0
    -
m, n: nat
F: nat -> nat
(forall i : nat, m <= i < n -> F i = 0) ->
\sum_(m <= i < n) F i = 0 move=> ZERO.
m, n: nat
F: nat -> nat
ZERO: forall i : nat, m <= i < n -> F i = 0
\sum_(m <= i < n) F i = 0
      have-> : \sum_(m <= i < n) F i = \sum_(m <= i < n) 0 by apply eq_big_nat.
m, n: nat
F: nat -> nat
ZERO: forall i : nat, m <= i < n -> F i = 0
\sum_(m <= i < n) 0 = 0
      exact: big1_eq.
  Qed.

  (** Moreover, the fact that the sum is smaller than the range of the summation
      implies the existence of a zero element. *)
  Lemma sum_le_summation_range:
    forall f t Δ,
      \sum_(t <= x < t + Δ) f x < Δ ->
      exists x, t <= x < t + Δ /\ f x = 0.
forall (f : nat -> nat) (t Δ : nat),
\sum_(t <= x < t + Δ) f x < Δ ->
exists x : nat, t <= x < t + Δ /\ f x = 0
  Proof.
forall (f : nat -> nat) (t Δ : nat),
\sum_(t <= x < t + Δ) f x < Δ ->
exists x : nat, t <= x < t + Δ /\ f x = 0
    induction Δ; intros; first by rewrite ltn0 in H.
f: nat -> nat
t, Δ: nat
IHΔ: \sum_(t <= x < t + Δ) f x < Δ -> exists x : nat, t <= x < t + Δ /\ f x = 0
H: \sum_(t <= x < t + Δ.+1) f x < Δ.+1
exists x : nat, t <= x < t + Δ.+1 /\ f x = 0
    destruct (f (t + Δ)) eqn: EQ.
f: nat -> nat
t, Δ: nat
IHΔ: \sum_(t <= x < t + Δ) f x < Δ -> exists x : nat, t <= x < t + Δ /\ f x = 0
H: \sum_(t <= x < t + Δ.+1) f x < Δ.+1
EQ: f (t + Δ) = 0
exists x : nat, t <= x < t + Δ.+1 /\ f x = 0
f: nat -> nat
t, Δ: nat
IHΔ: \sum_(t <= x < t + Δ) f x < Δ -> exists x : nat, t <= x < t + Δ /\ f x = 0
H: \sum_(t <= x < t + Δ.+1) f x < Δ.+1
n: nat
EQ: f (t + Δ) = n.+1
exists x : nat, t <= x < t + Δ.+1 /\ f x = 0
    {
f: nat -> nat
t, Δ: nat
IHΔ: \sum_(t <= x < t + Δ) f x < Δ -> exists x : nat, t <= x < t + Δ /\ f x = 0
H: \sum_(t <= x < t + Δ.+1) f x < Δ.+1
EQ: f (t + Δ) = 0
exists x : nat, t <= x < t + Δ.+1 /\ f x = 0 exists (t + Δ); split; last by done.
f: nat -> nat
t, Δ: nat
IHΔ: \sum_(t <= x < t + Δ) f x < Δ -> exists x : nat, t <= x < t + Δ /\ f x = 0
H: \sum_(t <= x < t + Δ.+1) f x < Δ.+1
EQ: f (t + Δ) = 0
t <= t + Δ < t + Δ.+1
      by apply/andP; split; [rewrite leq_addr | rewrite addnS ltnS]. }
f: nat -> nat
t, Δ: nat
IHΔ: \sum_(t <= x < t + Δ) f x < Δ -> exists x : nat, t <= x < t + Δ /\ f x = 0
H: \sum_(t <= x < t + Δ.+1) f x < Δ.+1
n: nat
EQ: f (t + Δ) = n.+1
exists x : nat, t <= x < t + Δ.+1 /\ f x = 0
    {
f: nat -> nat
t, Δ: nat
IHΔ: \sum_(t <= x < t + Δ) f x < Δ -> exists x : nat, t <= x < t + Δ /\ f x = 0
H: \sum_(t <= x < t + Δ.+1) f x < Δ.+1
n: nat
EQ: f (t + Δ) = n.+1
exists x : nat, t <= x < t + Δ.+1 /\ f x = 0 move: H; rewrite addnS big_nat_recr //= ?leq_addr // EQ addnS ltnS; move => H.
f: nat -> nat
t, Δ: nat
IHΔ: \sum_(t <= x < t + Δ) f x < Δ -> exists x : nat, t <= x < t + Δ /\ f x = 0
n: nat
EQ: f (t + Δ) = n.+1
H: \sum_(t <= i < t + Δ) f i + n < Δ
exists x : nat, t <= x < (t + Δ).+1 /\ f x = 0
      feed IHΔ.
f: nat -> nat
t, Δ: nat
IHΔ: \sum_(t <= x < t + Δ) f x < Δ -> exists x : nat, t <= x < t + Δ /\ f x = 0
n: nat
EQ: f (t + Δ) = n.+1
H: \sum_(t <= i < t + Δ) f i + n < Δ
\sum_(t <= x < t + Δ) f x < Δ
f: nat -> nat
t, Δ: nat
IHΔ: exists x : nat, t <= x < t + Δ /\ f x = 0
n: nat
EQ: f (t + Δ) = n.+1
H: \sum_(t <= i < t + Δ) f i + n < Δ
exists x : nat, t <= x < (t + Δ).+1 /\ f x = 0
      {
f: nat -> nat
t, Δ: nat
IHΔ: \sum_(t <= x < t + Δ) f x < Δ -> exists x : nat, t <= x < t + Δ /\ f x = 0
n: nat
EQ: f (t + Δ) = n.+1
H: \sum_(t <= i < t + Δ) f i + n < Δ
\sum_(t <= x < t + Δ) f x < Δ by apply leq_ltn_trans with (\sum_(t <= i < t + Δ) f i + n); first rewrite leq_addr. }
f: nat -> nat
t, Δ: nat
IHΔ: exists x : nat, t <= x < t + Δ /\ f x = 0
n: nat
EQ: f (t + Δ) = n.+1
H: \sum_(t <= i < t + Δ) f i + n < Δ
exists x : nat, t <= x < (t + Δ).+1 /\ f x = 0
      move: IHΔ => [z [/andP [LE GE] ZERO]].
f: nat -> nat
t, Δ, n: nat
EQ: f (t + Δ) = n.+1
H: \sum_(t <= i < t + Δ) f i + n < Δ
z: nat
LE: t <= z
GE: z < t + Δ
ZERO: f z = 0
exists x : nat, t <= x < (t + Δ).+1 /\ f x = 0
      exists z; split; last by done.
f: nat -> nat
t, Δ, n: nat
EQ: f (t + Δ) = n.+1
H: \sum_(t <= i < t + Δ) f i + n < Δ
z: nat
LE: t <= z
GE: z < t + Δ
ZERO: f z = 0
t <= z < (t + Δ).+1
      apply/andP; split; first by done.
f: nat -> nat
t, Δ, n: nat
EQ: f (t + Δ) = n.+1
H: \sum_(t <= i < t + Δ) f i + n < Δ
z: nat
LE: t <= z
GE: z < t + Δ
ZERO: f z = 0
z < (t + Δ).+1
      by rewrite ltnS ltnW. }
  Qed.

  (** Next, we prove that the summing over the difference of two functions is
      the same as summing over the two functions separately, and then taking the
      difference of the two sums. Since we are using natural numbers, we have to
      require that one function dominates the other in the summing range. *)
  Lemma sumnB_nat m n F G :
    (forall i, m <= i < n -> F i >= G i) ->
    \sum_(m <= i < n) (F i - G i) =
      (\sum_(m <= i < n) (F i)) - (\sum_(m <= i < n) (G i)).
m, n: nat
F, G: nat -> nat
(forall i : nat, m <= i < n -> G i <= F i) ->
\sum_(m <= i < n) (F i - G i) =
\sum_(m <= i < n) F i - \sum_(m <= i < n) G i
  Proof.
m, n: nat
F, G: nat -> nat
(forall i : nat, m <= i < n -> G i <= F i) ->
\sum_(m <= i < n) (F i - G i) =
\sum_(m <= i < n) F i - \sum_(m <= i < n) G i
    move=> le.
m, n: nat
F, G: nat -> nat
le: forall i : nat, m <= i < n -> G i <= F i
\sum_(m <= i < n) (F i - G i) =
\sum_(m <= i < n) F i - \sum_(m <= i < n) G i
    rewrite big_nat_cond [X in X - _]big_nat_cond [X in _ - X]big_nat_cond.
m, n: nat
F, G: nat -> nat
le: forall i : nat, m <= i < n -> G i <= F i
\sum_(m <= i < n | (m <= i < n) && true) (F i - G i) =
\sum_(m <= i < n | (m <= i < n) && true) F i -
\sum_(m <= i < n | (m <= i < n) && true) G i
    rewrite sumnB// => i; rewrite andbT; exact: le.
  Qed.

End SumsOverRanges.

(** In this section, we show how it is possible to equate the result of two sums performed
    on two different functions and on different intervals, provided that the two functions
    match point-wise. *)
Section SumOfTwoIntervals.

  (** Consider two equally-sized intervals <<[t1, t1+d)>> and <<[t2, t2+d)>>... *)
  Variable (t1 t2 : nat).
  Variable (d : nat).

  (** ...and two functions [F1] and [F2]. *)
  Variable (F1 F2 : nat -> nat).

  (** Assume that the two functions match point-wise with each other, with the points taken
      in their respective interval. *)
  Hypothesis equal_before_d: forall g, g < d -> F1 (t1 + g) = F2 (t2 + g).

  (** The then summations of [F1] over <<[t1, t1 + d)>> and [F2] over
      <<[t2, t2 + d)>> are equal. *)
  Lemma big_sum_eq_in_eq_sized_intervals:
    \sum_(t1 <= t < t1 + d) F1 t = \sum_(t2 <= t < t2 + d) F2 t.
t1, t2, d: nat
F1, F2: nat -> nat
equal_before_d: forall g : nat,
g < d -> F1 (t1 + g) = F2 (t2 + g)
\sum_(t1 <= t < t1 + d) F1 t =
\sum_(t2 <= t < t2 + d) F2 t
  Proof.
t1, t2, d: nat
F1, F2: nat -> nat
equal_before_d: forall g : nat,
g < d -> F1 (t1 + g) = F2 (t2 + g)
\sum_(t1 <= t < t1 + d) F1 t =
\sum_(t2 <= t < t2 + d) F2 t
    induction d; first by rewrite !addn0 !big_geq.
t1, t2, d: nat
F1, F2: nat -> nat
n: nat
equal_before_d: forall g : nat,
g < n.+1 -> F1 (t1 + g) = F2 (t2 + g)
IHn: (forall g : nat,
 g < n -> F1 (t1 + g) = F2 (t2 + g)) ->
\sum_(t1 <= t < t1 + n) F1 t =
\sum_(t2 <= t < t2 + n) F2 t
\sum_(t1 <= t < t1 + n.+1) F1 t =
\sum_(t2 <= t < t2 + n.+1) F2 t
    rewrite !addnS !big_nat_recr => //; try by lia.
t1, t2, d: nat
F1, F2: nat -> nat
n: nat
equal_before_d: forall g : nat,
g < n.+1 -> F1 (t1 + g) = F2 (t2 + g)
IHn: (forall g : nat,
 g < n -> F1 (t1 + g) = F2 (t2 + g)) ->
\sum_(t1 <= t < t1 + n) F1 t =
\sum_(t2 <= t < t2 + n) F2 t
addn_monoid
  (\big[addn_monoid/0]_(t1 <= i < t1 + n) F1 i)
  (F1 (t1 + n)) =
addn_monoid
  (\big[addn_monoid/0]_(t2 <= i < t2 + n) F2 i)
  (F2 (t2 + n))
    rewrite IHn //=; last by move=> g G_LTl; apply (equal_before_d g); lia.
t1, t2, d: nat
F1, F2: nat -> nat
n: nat
equal_before_d: forall g : nat,
g < n.+1 -> F1 (t1 + g) = F2 (t2 + g)
IHn: (forall g : nat,
 g < n -> F1 (t1 + g) = F2 (t2 + g)) ->
\sum_(t1 <= t < t1 + n) F1 t =
\sum_(t2 <= t < t2 + n) F2 t
\sum_(t2 <= t < t2 + n) F2 t + F1 (t1 + n) =
\sum_(t2 <= i < t2 + n) F2 i + F2 (t2 + n)
    by rewrite equal_before_d.
  Qed.

End SumOfTwoIntervals.


(** In this section, we relate the sum of items with the sum over partitions of those items. *)
Section SumOverPartitions.

  (** Consider an item type [X] and a partition type [Y]. *)
  Variable X Y : eqType.

  (** [x_to_y] is the mapping from an item to the partition it is contained in. *)
  Variable x_to_y : X -> Y.

  (** Consider [f], a function from [X] to [nat]. *)
  Variable f : X -> nat.

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

  (** Consider a sequence of items [xs] and a sequence of partitions [ys]. *)
  Variable xs : seq X.
  Variable ys : seq 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 -> x_to_y x \in ys.

  (** Consider the sum of [f x] over all [x] in a given partition [y]. *)
  Let sum_of_partition y := \sum_(x <- xs | P x && (x_to_y x == y)) f x.

  (** We prove that summation of [f x] over all [x] is less than or equal to the summation of
      [sum_of_partition] over all partitions. *)
  Lemma sum_over_partitions_le :
    \sum_(x <- xs | P x) f x
    <= \sum_(y <- ys) sum_of_partition y.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
\sum_(x <- xs | P x) f x <=
\sum_(y <- ys) sum_of_partition y
  Proof.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
\sum_(x <- xs | P x) f x <=
\sum_(y <- ys) sum_of_partition y
    rewrite /sum_of_partition.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
\sum_(x <- xs | P x) f x <=
\sum_(y <- ys)
   \sum_(x <- xs | P x && (x_to_y x == y)) f x
    induction xs as [| x' xs' LE_TAIL]; first by rewrite big_nil.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
LE_TAIL: (forall x : X, x \in xs' -> x_to_y x \in ys) ->
let sum_of_partition :=
  fun y : Y =>
  \sum_(x <- xs' | P x && (x_to_y x == y))
     f x in
\sum_(x <- xs' | P x) f x <=
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
\sum_(x <- (x' :: xs') | P x) f x <=
\sum_(y <- ys)
   \sum_(x <- (x' :: xs') | P x && (x_to_y x == y))
      f x
    have P_HOLDS: forall i j, true -> P j && (x_to_y j== i) -> P j by move=> ??? /andP [P_HOLDS _].
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
LE_TAIL: (forall x : X, x \in xs' -> x_to_y x \in ys) ->
let sum_of_partition :=
  fun y : Y =>
  \sum_(x <- xs' | P x && (x_to_y x == y))
     f x in
\sum_(x <- xs' | P x) f x <=
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
P_HOLDS: forall (i : Y) (j : X),
true -> P j && (x_to_y j == i) -> P j
\sum_(x <- (x' :: xs') | P x) f x <=
\sum_(y <- ys)
   \sum_(x <- (x' :: xs') | P x && (x_to_y x == y))
      f x
    have IN_ys: forall x : X, x \in xs' -> x_to_y x \in ys.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
LE_TAIL: (forall x : X, x \in xs' -> x_to_y x \in ys) ->
let sum_of_partition :=
  fun y : Y =>
  \sum_(x <- xs' | P x && (x_to_y x == y))
     f x in
\sum_(x <- xs' | P x) f x <=
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
P_HOLDS: forall (i : Y) (j : X),
true -> P j && (x_to_y j == i) -> P j
forall x : X, x \in xs' -> x_to_y x \in ys
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
LE_TAIL: (forall x : X, x \in xs' -> x_to_y x \in ys) ->
let sum_of_partition :=
  fun y : Y =>
  \sum_(x <- xs' | P x && (x_to_y x == y))
     f x in
\sum_(x <- xs' | P x) f x <=
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
P_HOLDS: forall (i : Y) (j : X),
true -> P j && (x_to_y j == i) -> P j
IN_ys: forall x : X, x \in xs' -> x_to_y x \in ys
\sum_(x <- (x' :: xs') | P x) f x <=
\sum_(y <- ys)
   \sum_(x <- (x' :: xs') | 
   P x && (x_to_y x == y)) 
   f x
    {
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
LE_TAIL: (forall x : X, x \in xs' -> x_to_y x \in ys) ->
let sum_of_partition :=
  fun y : Y =>
  \sum_(x <- xs' | P x && (x_to_y x == y))
     f x in
\sum_(x <- xs' | P x) f x <=
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
P_HOLDS: forall (i : Y) (j : X),
true -> P j && (x_to_y j == i) -> P j
forall x : X, x \in xs' -> x_to_y x \in ys by move=> ??; apply H_no_partition_missing => //; rewrite in_cons; apply /orP; right. }
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
LE_TAIL: (forall x : X, x \in xs' -> x_to_y x \in ys) ->
let sum_of_partition :=
  fun y : Y =>
  \sum_(x <- xs' | P x && (x_to_y x == y))
     f x in
\sum_(x <- xs' | P x) f x <=
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
P_HOLDS: forall (i : Y) (j : X),
true -> P j && (x_to_y j == i) -> P j
IN_ys: forall x : X, x \in xs' -> x_to_y x \in ys
\sum_(x <- (x' :: xs') | P x) f x <=
\sum_(y <- ys)
   \sum_(x <- (x' :: xs') | P x && (x_to_y x == y))
      f x
    move: LE_TAIL; rewrite (exchange_big_dep P) => //= LE_TAIL.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
P_HOLDS: forall (i : Y) (j : X),
true -> P j && (x_to_y j == i) -> P j
IN_ys: forall x : X, x \in xs' -> x_to_y x \in ys
LE_TAIL: (forall x : X, x \in xs' -> x_to_y x \in ys) ->
\sum_(x <- xs' | P x) f x <=
\sum_(j <- xs' | P j)
   \sum_(i <- ys | P j && (x_to_y j == i))
      f j
\sum_(x <- (x' :: xs') | P x) f x <=
\sum_(y <- ys)
   \sum_(x <- (x' :: xs') | P x && (x_to_y x == y))
      f x
    rewrite (exchange_big_dep P) //= !big_cons.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
P_HOLDS: forall (i : Y) (j : X),
true -> P j && (x_to_y j == i) -> P j
IN_ys: forall x : X, x \in xs' -> x_to_y x \in ys
LE_TAIL: (forall x : X, x \in xs' -> x_to_y x \in ys) ->
\sum_(x <- xs' | P x) f x <=
\sum_(j <- xs' | P j)
   \sum_(i <- ys | P j && (x_to_y j == i))
      f j
(if P x'
 then f x' + \sum_(j <- xs' | P j) f j
 else \sum_(j <- xs' | P j) f j) <=
(if P x'
 then
  \sum_(i <- ys | P x' && (x_to_y x' == i)) f x' +
  \sum_(j <- xs' | P j)
     \sum_(i <- ys | P j && (x_to_y j == i)) f j
 else
  \sum_(j <- xs' | P j)
     \sum_(i <- ys | P j && (x_to_y j == i)) f j)
    case: (P x') => //=; last by apply LE_TAIL.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
P_HOLDS: forall (i : Y) (j : X),
true -> P j && (x_to_y j == i) -> P j
IN_ys: forall x : X, x \in xs' -> x_to_y x \in ys
LE_TAIL: (forall x : X, x \in xs' -> x_to_y x \in ys) ->
\sum_(x <- xs' | P x) f x <=
\sum_(j <- xs' | P j)
   \sum_(i <- ys | P j && (x_to_y j == i))
      f j
f x' + \sum_(j <- xs' | P j) f j <=
\sum_(i <- ys | x_to_y x' == i) f x' +
\sum_(j <- xs' | P j)
   \sum_(i <- ys | P j && (x_to_y j == i)) f j
    apply leq_add => //; last by apply LE_TAIL.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
P_HOLDS: forall (i : Y) (j : X),
true -> P j && (x_to_y j == i) -> P j
IN_ys: forall x : X, x \in xs' -> x_to_y x \in ys
LE_TAIL: (forall x : X, x \in xs' -> x_to_y x \in ys) ->
\sum_(x <- xs' | P x) f x <=
\sum_(j <- xs' | P j)
   \sum_(i <- ys | P j && (x_to_y j == i))
      f j
f x' <= \sum_(i <- ys | x_to_y x' == i) f x'
    rewrite big_const_seq iter_addn_0.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
P_HOLDS: forall (i : Y) (j : X),
true -> P j && (x_to_y j == i) -> P j
IN_ys: forall x : X, x \in xs' -> x_to_y x \in ys
LE_TAIL: (forall x : X, x \in xs' -> x_to_y x \in ys) ->
\sum_(x <- xs' | P x) f x <=
\sum_(j <- xs' | P j)
   \sum_(i <- ys | P j && (x_to_y j == i))
      f j
f x' <= f x' * count (eq_op (x_to_y x')) ys
    apply leq_pmulr; rewrite -has_count.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
P_HOLDS: forall (i : Y) (j : X),
true -> P j && (x_to_y j == i) -> P j
IN_ys: forall x : X, x \in xs' -> x_to_y x \in ys
LE_TAIL: (forall x : X, x \in xs' -> x_to_y x \in ys) ->
\sum_(x <- xs' | P x) f x <=
\sum_(j <- xs' | P j)
   \sum_(i <- ys | P j && (x_to_y j == i))
      f j
has (eq_op (x_to_y x')) ys
    apply /hasP; eapply ex_intro2 => //.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
P_HOLDS: forall (i : Y) (j : X),
true -> P j && (x_to_y j == i) -> P j
IN_ys: forall x : X, x \in xs' -> x_to_y x \in ys
LE_TAIL: (forall x : X, x \in xs' -> x_to_y x \in ys) ->
\sum_(x <- xs' | P x) f x <=
\sum_(j <- xs' | P j)
   \sum_(i <- ys | P j && (x_to_y j == i))
      f j
x_to_y x' \in ys
    by apply H_no_partition_missing, mem_head.
  Qed.

  (** Consider a partition [y']. *)
  Variable y' : Y.

  (** We prove that the sum of items excluding all items from a partition [y']
      is less-than-or-equal to the sum over all partitions except [y']. *)
  Lemma reorder_summation : \sum_(x <- xs | P x && (x_to_y x != y')) f x <=
                \sum_(y <- ys | y != y') sum_of_partition y.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
\sum_(x <- xs | P x && (x_to_y x != y')) f x <=
\sum_(y <- ys | y != y') sum_of_partition y
  Proof.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
\sum_(x <- xs | P x && (x_to_y x != y')) f x <=
\sum_(y <- ys | y != y') sum_of_partition y
    rewrite (exchange_big_dep (fun x =>P x && (x_to_y x != y'))) //=.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
\sum_(x <- xs | P x && (x_to_y x != y')) f x <=
\sum_(j <- xs | P j && (x_to_y j != y'))
   \sum_(i <- ys | [&& i != y', P j & x_to_y j == i])
      f j
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
forall (i : Y) (j : X),
i != y' ->
P j && (x_to_y j == i) -> P j && (x_to_y j != y')
    -
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
\sum_(x <- xs | P x && (x_to_y x != y')) f x <=
\sum_(j <- xs | P j && (x_to_y j != y'))
   \sum_(i <- ys | [&& i != y', P j & x_to_y j == i])
      f j
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
forall (i : Y) (j : X),
i != y' ->
P j && (x_to_y j == i) -> P j && (x_to_y j != y') rewrite  big_seq_cond [X in _ <= X]big_seq_cond.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
\sum_(i <- xs | [&& i \in xs, P i & x_to_y i != y'])
   f i <=
\sum_(i <- xs | [&& i \in xs, P i & x_to_y i != y'])
   \sum_(i0 <- ys | [&& i0 != y', P i
                      & x_to_y i == i0]) f i
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
forall (i : Y) (j : X),
i != y' ->
P j && (x_to_y j == i) -> P j && (x_to_y j != y')
      apply leq_sum => x' /andP [ARRo /andP [Px' NEQ]].
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
x': X
ARRo: x' \in xs
Px': P x'
NEQ: x_to_y x' != y'
f x' <=
\sum_(i <- ys | [&& i != y', P x' & x_to_y x' == i])
   f x'
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
forall (i : Y) (j : X),
i != y' ->
P j && (x_to_y j == i) -> P j && (x_to_y j != y')
      rewrite (big_rem (x_to_y x')) //=.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
x': X
ARRo: x' \in xs
Px': P x'
NEQ: x_to_y x' != y'
f x' <=
(if
  [&& x_to_y x' != y', P x' & x_to_y x' == x_to_y x']
 then f x'
 else 0) +
\sum_(y <- rem (T:=Y) (x_to_y x') ys | [&& y != y',
                                           P x'
                                         & x_to_y x' ==
                                           y]) f x'
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
x': X
ARRo: x' \in xs
Px': P x'
NEQ: x_to_y x' != y'
x_to_y x' \in ys
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
forall (i : Y) (j : X),
i != y' ->
P j && (x_to_y j == i) -> P j && (x_to_y j != y')
      rewrite Px' eq_refl NEQ andTb andTb leq_addr //.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
x': X
ARRo: x' \in xs
Px': P x'
NEQ: x_to_y x' != y'
x_to_y x' \in ys
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
forall (i : Y) (j : X),
i != y' ->
P j && (x_to_y j == i) -> P j && (x_to_y j != y')
      by apply H_no_partition_missing.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
forall (i : Y) (j : X),
i != y' ->
P j && (x_to_y j == i) -> P j && (x_to_y j != y')
    -
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
forall (i : Y) (j : X),
i != y' ->
P j && (x_to_y j == i) -> P j && (x_to_y j != y') move => y_of_x' x' /negP NEQ /andP [EQ1 /eqP EQ2].
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y', y_of_x': Y
x': X
NEQ: ~ y_of_x' == y'
EQ1: P x'
EQ2: x_to_y x' = y_of_x'
P x' && (x_to_y x' != y')
      rewrite EQ1 Bool.andb_true_l; apply/negP; intros CONTR.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y', y_of_x': Y
x': X
NEQ: ~ y_of_x' == y'
EQ1: P x'
EQ2: x_to_y x' = y_of_x'
CONTR: x_to_y x' == y'
False
      apply: NEQ; clear EQ1.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y', y_of_x': Y
x': X
EQ2: x_to_y x' = y_of_x'
CONTR: x_to_y x' == y'
y_of_x' == y'
      by rewrite -EQ2.
  Qed.

  (** In this section, we prove a stronger result about the equality between
      the sum over all items and the sum over all partitions of those items. *)
  Section Equality.

    (** In order to prove the stronger result of equality, we additionally
        assume that the sequences [xs] and [ys] are sets, i.e., that each
        element is contained at most once. *)
    Hypothesis H_xs_unique : uniq xs.
    Hypothesis H_ys_unique : uniq ys.

    (** We prove that summation of [f x] over all [x] is equal to the summation of
      [sum_of_partition] over all partitions. *)
    Lemma sum_over_partitions_eq :
      \sum_(x <- xs | P x) f x
      = \sum_(y <- ys) sum_of_partition y.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq xs
H_ys_unique: uniq ys
\sum_(x <- xs | P x) f x =
\sum_(y <- ys) sum_of_partition y
    Proof.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq xs
H_ys_unique: uniq ys
\sum_(x <- xs | P x) f x =
\sum_(y <- ys) sum_of_partition y
      rewrite /sum_of_partition.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
H_no_partition_missing: forall x : X,
x \in xs -> x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- xs | P x &&
                (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq xs
H_ys_unique: uniq ys
\sum_(x <- xs | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs | P x && (x_to_y x == y)) f x
      induction xs as [|x' xs' LE_TAIL]; first by rewrite big_nil big1_seq //= => ??; rewrite big_nil.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: (forall x : X, x \in xs' -> x_to_y x \in ys) ->
let sum_of_partition :=
  fun y : Y =>
  \sum_(x <- xs' | P x && (x_to_y x == y))
     f x in
uniq xs' ->
\sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
\sum_(x <- (x' :: xs') | P x) f x =
\sum_(y <- ys)
   \sum_(x <- (x' :: xs') | P x && (x_to_y x == y))
      f x
      rewrite //= in LE_TAIL; feed_n 2 LE_TAIL.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: (forall x : X, x \in xs' -> x_to_y x \in ys) ->
uniq xs' ->
\sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
forall x : X, x \in xs' -> x_to_y x \in ys
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: uniq xs' ->
\sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
uniq xs'
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: \sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
\sum_(x <- (x' :: xs') | P x) f x =
\sum_(y <- ys)
   \sum_(x <- (x' :: xs') | 
   P x && (x_to_y x == y)) 
   f x
      {
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: (forall x : X, x \in xs' -> x_to_y x \in ys) ->
uniq xs' ->
\sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
forall x : X, x \in xs' -> x_to_y x \in ys by move => ??; apply H_no_partition_missing; rewrite in_cons; apply /orP; right. }
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: uniq xs' ->
\sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
uniq xs'
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: \sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
\sum_(x <- (x' :: xs') | P x) f x =
\sum_(y <- ys)
   \sum_(x <- (x' :: xs') | 
   P x && (x_to_y x == y)) 
   f x
      {
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: uniq xs' ->
\sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
uniq xs' by move: H_xs_unique; rewrite cons_uniq => /andP [??]. }
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: \sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
\sum_(x <- (x' :: xs') | P x) f x =
\sum_(y <- ys)
   \sum_(x <- (x' :: xs') | P x && (x_to_y x == y))
      f x
      rewrite (exchange_big_dep P) //=; last by move=> ??? /andP[??].
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: \sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
\sum_(x <- (x' :: xs') | P x) f x =
\sum_(j <- (x' :: xs') | P j)
   \sum_(i <- ys | P j && (x_to_y j == i)) f j
      rewrite !big_cons.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: \sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
(if P x'
 then f x' + \sum_(j <- xs' | P j) f j
 else \sum_(j <- xs' | P j) f j) =
(if P x'
 then
  \sum_(i <- ys | P x' && (x_to_y x' == i)) f x' +
  \sum_(j <- xs' | P j)
     \sum_(i <- ys | P j && (x_to_y j == i)) f j
 else
  \sum_(j <- xs' | P j)
     \sum_(i <- ys | P j && (x_to_y j == i)) f j)
      destruct (P x'); last by rewrite LE_TAIL (exchange_big_dep P) //=;  move=> ??? /andP[??].
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: \sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
f x' + \sum_(j <- xs' | P j) f j =
\sum_(i <- ys | true && (x_to_y x' == i)) f x' +
\sum_(j <- xs' | P j)
   \sum_(i <- ys | P j && (x_to_y j == i)) f j
      have -> : \sum_(i <- ys | true && ( x_to_y x' == i)) f x' = f x'.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: \sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
\sum_(i <- ys | true && (x_to_y x' == i)) f x' = f x'
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: \sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
f x' + \sum_(j <- xs' | P j) f j =
f x' +
\sum_(j <- xs' | P j)
   \sum_(i <- ys | P j && (x_to_y j == i)) f j
      {
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: \sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
\sum_(i <- ys | true && (x_to_y x' == i)) f x' = f x' rewrite //= -big_filter.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: \sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
\sum_(i <- [seq x <- ys | x_to_y x' == x]) f x' = f x'
        have -> : [seq i <- ys | x_to_y x' == i] = [:: x_to_y x']; last by rewrite unlock //= addn0.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: \sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
[seq i <- ys | x_to_y x' == i] = [:: x_to_y x']
        have -> : [seq i <- ys | x_to_y x' == i] = [seq i <- ys | i == x_to_y x'].
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: \sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
[seq i <- ys | x_to_y x' == i] =
[seq i <- ys | i == x_to_y x']
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: \sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
[seq i <- ys | i == x_to_y x'] = [:: x_to_y x']
        {
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: \sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
[seq i <- ys | x_to_y x' == i] =
[seq i <- ys | i == x_to_y x'] clear H_no_partition_missing LE_TAIL.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
[seq i <- ys | x_to_y x' == i] =
[seq i <- ys | i == x_to_y x']
          induction ys as [| y'' ys' LE_TAILy]; first by done.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
y'': Y
ys': seq Y
H_ys_unique: uniq (y'' :: ys')
LE_TAILy: uniq ys' ->
[seq i <- ys' | x_to_y x' == i] =
[seq i <- ys' | i == x_to_y x']
[seq i <- y'' :: ys' | x_to_y x' == i] =
[seq i <- y'' :: ys' | i == x_to_y x']
          feed LE_TAILy; first by move: H_ys_unique; rewrite cons_uniq => /andP [??].
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
y'': Y
ys': seq Y
H_ys_unique: uniq (y'' :: ys')
LE_TAILy: [seq i <- ys' | x_to_y x' == i] =
[seq i <- ys' | i == x_to_y x']
[seq i <- y'' :: ys' | x_to_y x' == i] =
[seq i <- y'' :: ys' | i == x_to_y x']
          by rewrite //=  LE_TAILy //= eq_sym. }
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: \sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
[seq i <- ys | i == x_to_y x'] = [:: x_to_y x']
        apply filter_pred1_uniq => //.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: \sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
x_to_y x' \in ys
        by apply H_no_partition_missing; rewrite in_cons; apply /orP; left. }
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: \sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
f x' + \sum_(j <- xs' | P j) f j =
f x' +
\sum_(j <- xs' | P j)
   \sum_(i <- ys | P j && (x_to_y j == i)) f j
      apply /eqP; rewrite eqn_add2l; apply /eqP.
X, Y: eqType
x_to_y: X -> Y
f: X -> nat
P: pred X
xs: seq X
ys: seq Y
x': X
xs': seq X
H_no_partition_missing: forall x : X,
x \in x' :: xs' ->
x_to_y x \in ys
sum_of_partition:= fun y : Y =>
\sum_(x <- (x' :: xs') | 
P x && (x_to_y x == y)) 
f x: Y -> nat
y': Y
H_xs_unique: uniq (x' :: xs')
H_ys_unique: uniq ys
LE_TAIL: \sum_(x <- xs' | P x) f x =
\sum_(y <- ys)
   \sum_(x <- xs' | P x && (x_to_y x == y))
      f x
\sum_(j <- xs' | P j) f j =
\sum_(j <- xs' | P j)
   \sum_(i <- ys | P j && (x_to_y j == i)) f j
      by rewrite LE_TAIL (exchange_big_dep P) //=;  move=> ??? /andP[??].
    Qed.

  End Equality.

End SumOverPartitions.

(** We observe a trivial monotonicity-preserving property with regard to
    [leq]. *)
Section Monotonicity.

  (** Consider any type of indices, any predicate, ... *)
  Variables (I : eqType) (P : pred I).

  (** ... and any function that maps each index to a [nat -> nat] function. *)
  Variable F : I -> nat -> nat.

  (** Consider any set of indices ... *)
  Variable r : seq I.

  (** ... and suppose that [F i] is monotonic with regard to [leq] for every
      index in [r]. *)
  Hypothesis H_mono : forall i, i \in r -> monotone leq (F i).

  (** Consider the sum of [F] over [r], for any given [x]. *)
  Let f x := \sum_(i <- r | P i) F i x.

  (** We note that this sum [f] is monotonic with regard to [leq] in [x]. *)
  Lemma sum_leq_mono :
    monotone leq f.
I: eqType
P: pred I
F: I -> nat -> nat
r: seq I
H_mono: forall i : I, i \in r -> monotone leq (F i)
f:= fun x : nat => \sum_(i <- r | P i) F i x: nat -> nat
monotone leq f
  Proof.
I: eqType
P: pred I
F: I -> nat -> nat
r: seq I
H_mono: forall i : I, i \in r -> monotone leq (F i)
f:= fun x : nat => \sum_(i <- r | P i) F i x: nat -> nat
monotone leq f
    move=> x y LEQ.
I: eqType
P: pred I
F: I -> nat -> nat
r: seq I
H_mono: forall i : I, i \in r -> monotone leq (F i)
f:= fun x : nat => \sum_(i <- r | P i) F i x: nat -> nat
x, y: nat
LEQ: x <= y
f x <= f y
    rewrite /f big_seq_cond [in X in _ <= X]big_seq_cond.
I: eqType
P: pred I
F: I -> nat -> nat
r: seq I
H_mono: forall i : I, i \in r -> monotone leq (F i)
f:= fun x : nat => \sum_(i <- r | P i) F i x: nat -> nat
x, y: nat
LEQ: x <= y
\sum_(i <- r | (i \in r) && P i) F i x <=
\sum_(i <- r | (i \in r) && P i) F i y
    apply: leq_sum => i /andP [IN _].
I: eqType
P: pred I
F: I -> nat -> nat
r: seq I
H_mono: forall i : I, i \in r -> monotone leq (F i)
f:= fun x : nat => \sum_(i <- r | P i) F i x: nat -> nat
x, y: nat
LEQ: x <= y
i: I
IN: i \in r
F i x <= F i y
    by apply: H_mono.
  Qed.

End Monotonicity.