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

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]

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 :
      all (fun x => F x == 0) r = (\sum_(i <- r) F i == 0).
I: eqType
r: seq I
P: pred I
F: I -> nat
all (fun x : I => F x == 0) r =
(\sum_(i <- r) F i == 0)
    Proof.
I: eqType
r: seq I
P: pred I
F: I -> nat
all (fun x : I => F x == 0) r =
(\sum_(i <- r) F i == 0)
      destruct (all (fun x => F x == 0) r) eqn:ZERO.
I: eqType
r: seq I
P: pred I
F: I -> nat
ZERO: all (fun x : I => F x == 0) r = true
true = (\sum_(i <- r) F i == 0)
I: eqType
r: seq I
P: pred I
F: I -> nat
ZERO: all (fun x : I => F x == 0) r = false
false = (\sum_(i <- r) F i == 0)
      {
I: eqType
r: seq I
P: pred I
F: I -> nat
ZERO: all (fun x : I => F x == 0) r = true
true = (\sum_(i <- r) F i == 0) move: ZERO => /allP ZERO; rewrite -leqn0.
I: eqType
r: seq I
P: pred I
F: I -> nat
ZERO: {in r, forall x : I, F x == 0}
true = (\sum_(i <- r) F i <= 0)
        rewrite big_seq_cond (eq_bigr (fun x => 0)); first by rewrite big_const_seq iter_addn.
I: eqType
r: seq I
P: pred I
F: I -> nat
ZERO: {in r, forall x : I, F x == 0}
forall i : I, (i \in r) && true -> F i = 0
        move=> i; rewrite andbT=>IN.
I: eqType
r: seq I
P: pred I
F: I -> nat
ZERO: {in r, forall x : I, F x == 0}
i: I
IN: i \in r
F i = 0
        specialize (ZERO i); rewrite IN in ZERO.
I: eqType
r: seq I
P: pred I
F: I -> nat
i: I
IN: i \in r
ZERO: true -> F i == 0
F i = 0
        by move: ZERO => /implyP ZERO; apply/eqP; apply ZERO. }
I: eqType
r: seq I
P: pred I
F: I -> nat
ZERO: all (fun x : I => F x == 0) r = false
false = (\sum_(i <- r) F i == 0)
      {
I: eqType
r: seq I
P: pred I
F: I -> nat
ZERO: all (fun x : I => F x == 0) r = false
false = (\sum_(i <- r) F i == 0) apply negbT in ZERO; rewrite -has_predC in ZERO.
I: eqType
r: seq I
P: pred I
F: I -> nat
ZERO: has (predC (fun x : I => F x == 0)) r
false = (\sum_(i <- r) F i == 0)
        move: ZERO => /hasP [x IN NEQ].
I: eqType
r: seq I
P: pred I
F: I -> nat
x: I
IN: x \in r
NEQ: predC (fun x : I => F x == 0) x
false = (\sum_(i <- r) F i == 0)
        rewrite (big_rem x) //=.
I: eqType
r: seq I
P: pred I
F: I -> nat
x: I
IN: x \in r
NEQ: predC (fun x : I => F x == 0) x
false = (F x + \sum_(y <- rem (T:=I) x r) F y == 0)
        symmetry; apply negbTE; rewrite neq_ltn; apply/orP; right.
I: eqType
r: seq I
P: pred I
F: I -> nat
x: I
IN: x \in r
NEQ: predC (fun x : I => F x == 0) x
0 < F x + \sum_(y <- rem (T:=I) x r) F y
        apply leq_trans with (n := F x); last by apply leq_addr.
I: eqType
r: seq I
P: pred I
F: I -> nat
x: I
IN: x \in r
NEQ: predC (fun x : I => F x == 0) x
0 < F x
        by rewrite lt0n. }
    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_seq_gt0P:
      reflect (exists i, i \in r /\ 0 < F i) (0 < \sum_(i <- r) F i).
I: eqType
r: seq I
P: pred I
F: I -> nat
reflect (exists i : I, i \in r /\ 0 < F i)
  (0 < \sum_(i <- r) F i)
    Proof.
I: eqType
r: seq I
P: pred I
F: I -> nat
reflect (exists i : I, i \in r /\ 0 < F i)
  (0 < \sum_(i <- r) F i)
      apply: (iffP idP); move=> LT0.
I: eqType
r: seq I
P: pred I
F: I -> nat
LT0: 0 < \sum_(i <- r) F i
exists i : I, i \in r /\ 0 < F i
I: eqType
r: seq I
P: pred I
F: I -> nat
LT0: exists i : I, i \in r /\ 0 < F i
0 < \sum_(i <- r) F i
      {
I: eqType
r: seq I
P: pred I
F: I -> nat
LT0: 0 < \sum_(i <- r) F i
exists i : I, i \in r /\ 0 < F i induction r; first by rewrite big_nil in LT0.
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
l: seq I
LT0: 0 < \sum_(i <- (a :: l)) F i
IHl: 0 < \sum_(i <- l) F i -> exists i : I, i \in l /\ 0 < F i
exists i : I, i \in a :: l /\ 0 < F i
        destruct (F a > 0) eqn:POS.
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
l: seq I
LT0: 0 < \sum_(i <- (a :: l)) F i
IHl: 0 < \sum_(i <- l) F i -> exists i : I, i \in l /\ 0 < F i
POS: (0 < F a) = true
exists i : I, i \in a :: l /\ 0 < F i
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
l: seq I
LT0: 0 < \sum_(i <- (a :: l)) F i
IHl: 0 < \sum_(i <- l) F i -> exists i : I, i \in l /\ 0 < F i
POS: (0 < F a) = false
exists i : I, i \in a :: l /\ 0 < F i
        -
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
l: seq I
LT0: 0 < \sum_(i <- (a :: l)) F i
IHl: 0 < \sum_(i <- l) F i -> exists i : I, i \in l /\ 0 < F i
POS: (0 < F a) = true
exists i : I, i \in a :: l /\ 0 < F i
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
l: seq I
LT0: 0 < \sum_(i <- (a :: l)) F i
IHl: 0 < \sum_(i <- l) F i -> exists i : I, i \in l /\ 0 < F i
POS: (0 < F a) = false
exists i : I, i \in a :: l /\ 0 < F i exists a.
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
l: seq I
LT0: 0 < \sum_(i <- (a :: l)) F i
IHl: 0 < \sum_(i <- l) F i -> exists i : I, i \in l /\ 0 < F i
POS: (0 < F a) = true
a \in a :: l /\ 0 < F a
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
l: seq I
LT0: 0 < \sum_(i <- (a :: l)) F i
IHl: 0 < \sum_(i <- l) F i -> exists i : I, i \in l /\ 0 < F i
POS: (0 < F a) = false
exists i : I, i \in a :: l /\ 0 < F i
          by split => //; rewrite in_cons; apply /orP; left.
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
l: seq I
LT0: 0 < \sum_(i <- (a :: l)) F i
IHl: 0 < \sum_(i <- l) F i -> exists i : I, i \in l /\ 0 < F i
POS: (0 < F a) = false
exists i : I, i \in a :: l /\ 0 < F i
        -
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
l: seq I
LT0: 0 < \sum_(i <- (a :: l)) F i
IHl: 0 < \sum_(i <- l) F i -> exists i : I, i \in l /\ 0 < F i
POS: (0 < F a) = false
exists i : I, i \in a :: l /\ 0 < F i apply negbT in POS; rewrite -leqNgt leqn0 in POS; move: POS => /eqP POS.
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
l: seq I
LT0: 0 < \sum_(i <- (a :: l)) F i
IHl: 0 < \sum_(i <- l) F i -> exists i : I, i \in l /\ 0 < F i
POS: F a = 0
exists i : I, i \in a :: l /\ 0 < F i
          rewrite big_cons POS add0n in LT0.
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
l: seq I
IHl: 0 < \sum_(i <- l) F i -> exists i : I, i \in l /\ 0 < F i
POS: F a = 0
LT0: 0 < \sum_(j <- l) F j
exists i : I, i \in a :: l /\ 0 < F i
          move: (IHl LT0) => [i [IN POSi]].
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
l: seq I
IHl: 0 < \sum_(i <- l) F i -> exists i : I, i \in l /\ 0 < F i
POS: F a = 0
LT0: 0 < \sum_(j <- l) F j
i: I
IN: i \in l
POSi: 0 < F i
exists i : I, i \in a :: l /\ 0 < F i
          by exists i; split => //; rewrite in_cons; apply /orP; right. }
I: eqType
r: seq I
P: pred I
F: I -> nat
LT0: exists i : I, i \in r /\ 0 < F i
0 < \sum_(i <- r) F i
      {
I: eqType
r: seq I
P: pred I
F: I -> nat
LT0: exists i : I, i \in r /\ 0 < F i
0 < \sum_(i <- r) F i move: LT0 => [i [IN POS]].
I: eqType
r: seq I
P: pred I
F: I -> nat
i: I
IN: i \in r
POS: 0 < F i
0 < \sum_(i <- r) F i
        rewrite (big_rem i) //=.
I: eqType
r: seq I
P: pred I
F: I -> nat
i: I
IN: i \in r
POS: 0 < F i
0 < F i + \sum_(y <- rem (T:=I) i r) F y
        by apply leq_trans with (F i); last by rewrite leq_addr. }
    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:
      forall 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
forall 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
forall a : I,
a \notin r ->
\sum_(x <- r | P x && (x != a)) F x =
\sum_(x <- r | P x) F x
      intros a NOTIN.
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
NOTIN: a \notin r
\sum_(x <- r | P x && (x != a)) F x =
\sum_(x <- r | P x) F x
      induction r; first by rewrite !big_nil.
I: eqType
r: seq I
P: pred I
F: I -> nat
a, a0: I
l: seq I
NOTIN: a \notin a0 :: l
IHl: a \notin l ->
\sum_(x <- l | P x && (x != a)) F x =
\sum_(x <- l | P x) F x
\sum_(x <- (a0 :: l) | P x && (x != a)) F x =
\sum_(x <- (a0 :: l) | P x) F x
      rewrite !big_cons IHl.
I: eqType
r: seq I
P: pred I
F: I -> nat
a, a0: I
l: seq I
NOTIN: a \notin a0 :: l
IHl: a \notin l ->
\sum_(x <- l | P x && (x != a)) F x =
\sum_(x <- l | P x) F x
(if P a0 && (a0 != a)
 then F a0 + \sum_(x <- l | P x) F x
 else \sum_(x <- l | P x) F x) =
(if P a0
 then F a0 + \sum_(j <- l | P j) F j
 else \sum_(j <- l | P j) F j)
I: eqType
r: seq I
P: pred I
F: I -> nat
a, a0: I
l: seq I
NOTIN: a \notin a0 :: l
IHl: a \notin l ->
\sum_(x <- l | P x && (x != a)) F x =
\sum_(x <- l | P x) F x
a \notin l
      {
I: eqType
r: seq I
P: pred I
F: I -> nat
a, a0: I
l: seq I
NOTIN: a \notin a0 :: l
IHl: a \notin l ->
\sum_(x <- l | P x && (x != a)) F x =
\sum_(x <- l | P x) F x
(if P a0 && (a0 != a)
 then F a0 + \sum_(x <- l | P x) F x
 else \sum_(x <- l | P x) F x) =
(if P a0
 then F a0 + \sum_(j <- l | P j) F j
 else \sum_(j <- l | P j) F j) move: NOTIN => /memPn NOTIN.
I: eqType
r: seq I
P: pred I
F: I -> nat
a, a0: I
l: seq I
IHl: a \notin l -> \sum_(x <- l | P x && (x != a)) F x = \sum_(x <- l | P x) F x
NOTIN: {in a0 :: l, forall y : I, y != a}
(if P a0 && (a0 != a)
 then F a0 + \sum_(x <- l | P x) F x
 else \sum_(x <- l | P x) F x) =
(if P a0
 then F a0 + \sum_(j <- l | P j) F j
 else \sum_(j <- l | P j) F j) 
        move: (NOTIN a0) => NEQ.
I: eqType
r: seq I
P: pred I
F: I -> nat
a, a0: I
l: seq I
IHl: a \notin l -> \sum_(x <- l | P x && (x != a)) F x = \sum_(x <- l | P x) F x
NOTIN: {in a0 :: l, forall y : I, y != a}
NEQ: a0 \in a0 :: l -> a0 != a
(if P a0 && (a0 != a)
 then F a0 + \sum_(x <- l | P x) F x
 else \sum_(x <- l | P x) F x) =
(if P a0
 then F a0 + \sum_(j <- l | P j) F j
 else \sum_(j <- l | P j) F j)
        feed NEQ; first by (rewrite in_cons; apply/orP; left).
I: eqType
r: seq I
P: pred I
F: I -> nat
a, a0: I
l: seq I
IHl: a \notin l -> \sum_(x <- l | P x && (x != a)) F x = \sum_(x <- l | P x) F x
NOTIN: {in a0 :: l, forall y : I, y != a}
NEQ: a0 != a
(if P a0 && (a0 != a)
 then F a0 + \sum_(x <- l | P x) F x
 else \sum_(x <- l | P x) F x) =
(if P a0
 then F a0 + \sum_(j <- l | P j) F j
 else \sum_(j <- l | P j) F j)
        by rewrite NEQ Bool.andb_true_r. }
I: eqType
r: seq I
P: pred I
F: I -> nat
a, a0: I
l: seq I
NOTIN: a \notin a0 :: l
IHl: a \notin l ->
\sum_(x <- l | P x && (x != a)) F x =
\sum_(x <- l | P x) F x
a \notin l
      {
I: eqType
r: seq I
P: pred I
F: I -> nat
a, a0: I
l: seq I
NOTIN: a \notin a0 :: l
IHl: a \notin l ->
\sum_(x <- l | P x && (x != a)) F x =
\sum_(x <- l | P x) F x
a \notin l apply /memPn; intros y IN.
I: eqType
r: seq I
P: pred I
F: I -> nat
a, a0: I
l: seq I
NOTIN: a \notin a0 :: l
IHl: a \notin l ->
\sum_(x <- l | P x && (x != a)) F x =
\sum_(x <- l | P x) F x
y: I
IN: y \in l
y != a
        move: NOTIN => /memPn NOTIN.
I: eqType
r: seq I
P: pred I
F: I -> nat
a, a0: I
l: seq I
IHl: a \notin l -> \sum_(x <- l | P x && (x != a)) F x = \sum_(x <- l | P x) F x
y: I
IN: y \in l
NOTIN: {in a0 :: l, forall y : I, y != a}
y != a
        by apply NOTIN; rewrite in_cons; apply/orP; right. }
    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:
      forall 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
forall 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
forall 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]
      intros.
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
H: 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]
      induction r; first by rewrite big_nil.
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: (forall a : I, a \in l -> P a -> F a <= c) ->
\sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
\sum_(j <- (a :: l) | P j) F j <=
c * size [seq j <- a :: l | P j]
      feed IHl.
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: (forall a : I, a \in l -> P a -> F a <= c) ->
\sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
forall a : I, a \in l -> P a -> F a <= c
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: \sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
\sum_(j <- (a :: l) | P j) F j <=
c * size [seq j <- a :: l | P j]
      {
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: (forall a : I, a \in l -> P a -> F a <= c) ->
\sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
forall a : I, a \in l -> P a -> F a <= c intros; apply H.
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: (forall a : I, a \in l -> P a -> F a <= c) ->
\sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
a0: I
H0: a0 \in l
H1: P a0
a0 \in a :: l
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: (forall a : I, a \in l -> P a -> F a <= c) ->
\sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
a0: I
H0: a0 \in l
H1: P a0
P a0
        -
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: (forall a : I, a \in l -> P a -> F a <= c) ->
\sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
a0: I
H0: a0 \in l
H1: P a0
a0 \in a :: l
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: (forall a : I, a \in l -> P a -> F a <= c) ->
\sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
a0: I
H0: a0 \in l
H1: P a0
P a0 by rewrite in_cons; apply/orP; right.
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: (forall a : I, a \in l -> P a -> F a <= c) ->
\sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
a0: I
H0: a0 \in l
H1: P a0
P a0
        -
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: (forall a : I, a \in l -> P a -> F a <= c) ->
\sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
a0: I
H0: a0 \in l
H1: P a0
P a0 by done. }
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: \sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
\sum_(j <- (a :: l) | P j) F j <=
c * size [seq j <- a :: l | P j] 
      rewrite big_cons.
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: \sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
(if P a
 then F a + \sum_(j <- l | P j) F j
 else \sum_(j <- l | P j) F j) <=
c * size [seq j <- a :: l | P j]
      destruct (P a) eqn:EQ.
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: \sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
EQ: P a = true
F a + \sum_(j <- l | P j) F j <=
c * size [seq j <- a :: l | P j]
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: \sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
EQ: P a = false
\sum_(j <- l | P j) F j <=
c * size [seq j <- a :: l | P j]
      {
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: \sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
EQ: P a = true
F a + \sum_(j <- l | P j) F j <=
c * size [seq j <- a :: l | P j] rewrite -cat1s filter_cat size_cat mulnDr.
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: \sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
EQ: P a = true
F a + \sum_(j <- l | P j) F j <=
c * size [seq j <- [:: a] | P j] +
c * size [seq j <- l | P j]
        apply leq_add; last by done.
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: \sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
EQ: P a = true
F a <= c * size [seq j <- [:: a] | P j]
        rewrite size_filter //= EQ addn0 muln1.
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: \sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
EQ: P a = true
F a <= c
        apply H; last by done.
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: \sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
EQ: P a = true
a \in a :: l 
        by rewrite in_cons; apply/orP; left. }
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: \sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
EQ: P a = false
\sum_(j <- l | P j) F j <=
c * size [seq j <- a :: l | P j]
      {
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: \sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
EQ: P a = false
\sum_(j <- l | P j) F j <=
c * size [seq j <- a :: l | P j] apply leq_trans with (c * size [seq j <- l | P j]); first by done.
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: \sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
EQ: P a = false
c * size [seq j <- l | P j] <=
c * size [seq j <- a :: l | P j]
        rewrite leq_mul2l; apply /orP; right.
I: eqType
r: seq I
P: pred I
F: I -> nat
c: nat
a: I
l: seq I
H: forall a0 : I, a0 \in a :: l -> P a0 -> F a0 <= c
IHl: \sum_(j <- l | P j) F j <= c * size [seq j <- l | P j]
EQ: P a = false
size [seq j <- l | P j] <=
size [seq j <- a :: l | P j]
        by rewrite -cat1s filter_cat size_cat leq_addl. }
    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
      induction r; first by rewrite !big_nil subn0.
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
l: seq I
IHl: \sum_(r <- l | P r) F r = \sum_(r <- l) F r - \sum_(r <- l | ~~ P r) F r
\sum_(r <- (a :: l) | P r) F r =
\sum_(r <- (a :: l)) F r -
\sum_(r <- (a :: l) | ~~ P r) F r
      rewrite !big_cons !IHl; clear IHl.
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
l: seq I
(if P a
 then
  F a +
  (\sum_(r <- l) F r - \sum_(r <- l | ~~ P r) F r)
 else \sum_(r <- l) F r - \sum_(r <- l | ~~ P r) F r) =
F a + \sum_(j <- l) F j -
(if ~~ P a
 then F a + \sum_(j <- l | ~~ P j) F j
 else \sum_(j <- l | ~~ P j) F j)
      case (P a); simpl; last by rewrite subnDl.
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
l: seq I
F a + (\sum_(r <- l) F r - \sum_(r <- l | ~~ P r) F r) =
F a + \sum_(j <- l) F j - \sum_(j <- l | ~~ P j) F j
      rewrite addnBA; first by done.
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
l: seq I
\sum_(r <- l | ~~ P r) F r <= \sum_(r <- l) F r
      rewrite big_mkcond leq_sum //.
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
l: seq I
forall i : I,
true -> (if ~~ P i then F i else 0) <= F i
      intros t _.
I: eqType
r: seq I
P: pred I
F: I -> nat
a: I
l: seq I
t: I
(if ~~ P t then F t else 0) <= F t
      by case (P t).
    Qed.

    (** Summing natural numbers over a superset can only yields a greater sum.
        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 :
      forall (rs: seq I),
        uniq r ->
        {subset r <= rs} ->
        \sum_(i <- r) F i <= \sum_(i <- rs) F i.
I: eqType
r: seq I
P: pred I
F: I -> nat
forall rs : seq I,
uniq r ->
{subset r <= rs} ->
\sum_(i <- r) F i <= \sum_(i <- rs) F i
    Proof.
I: eqType
r: seq I
P: pred I
F: I -> nat
forall rs : seq I,
uniq r ->
{subset r <= rs} ->
\sum_(i <- r) F i <= \sum_(i <- rs) F i
      intros rs UNIQ SUB; generalize dependent rs.
I: eqType
r: seq I
P: pred I
F: I -> nat
UNIQ: uniq r
forall rs : seq I,
{subset r <= rs} ->
\sum_(i <- r) F i <= \sum_(i <- rs) F i
      induction r as [| x r1' IH]; first by ins; rewrite big_nil.
I: eqType
r: seq I
P: pred I
F: I -> nat
x: I
r1': seq I
UNIQ: uniq (x :: r1')
IH: uniq r1' ->
forall rs : seq I,
{subset r1' <= rs} ->
\sum_(i <- r1') F i <= \sum_(i <- rs) F i
forall rs : seq I,
{subset x :: r1' <= rs} ->
\sum_(i <- (x :: r1')) F i <= \sum_(i <- rs) F i
      intros rs SUB.
I: eqType
r: seq I
P: pred I
F: I -> nat
x: I
r1': seq I
UNIQ: uniq (x :: r1')
IH: uniq r1' ->
forall rs : seq I,
{subset r1' <= rs} ->
\sum_(i <- r1') F i <= \sum_(i <- rs) F i
rs: seq I
SUB: {subset x :: r1' <= rs}
\sum_(i <- (x :: r1')) F i <= \sum_(i <- rs) F i
      have IN: x \in rs by apply SUB; rewrite in_cons eq_refl orTb.
I: eqType
r: seq I
P: pred I
F: I -> nat
x: I
r1': seq I
UNIQ: uniq (x :: r1')
IH: uniq r1' ->
forall rs : seq I,
{subset r1' <= rs} ->
\sum_(i <- r1') F i <= \sum_(i <- rs) F i
rs: seq I
SUB: {subset x :: r1' <= rs}
IN: x \in rs
\sum_(i <- (x :: r1')) F i <= \sum_(i <- rs) F i
      simpl in UNIQ; move: UNIQ => /andP [NOTIN UNIQ]; specialize (IH UNIQ).
I: eqType
r: seq I
P: pred I
F: I -> nat
x: I
r1': seq I
IH: forall rs : seq I,
{subset r1' <= rs} ->
\sum_(i <- r1') F i <= \sum_(i <- rs) F i
rs: seq I
SUB: {subset x :: r1' <= rs}
IN: x \in rs
NOTIN: x \notin r1'
UNIQ: uniq r1'
\sum_(i <- (x :: r1')) F i <= \sum_(i <- rs) F i
      destruct (splitPr IN).
I: eqType
r: seq I
P: pred I
F: I -> nat
x: I
r1': seq I
IH: forall rs : seq I,
{subset r1' <= rs} ->
\sum_(i <- r1') F i <= \sum_(i <- rs) F i
p1, p2: seq I
SUB: {subset x :: r1' <= p1 ++ x :: p2}
IN: x \in p1 ++ x :: p2
NOTIN: x \notin r1'
UNIQ: uniq r1'
\sum_(i <- (x :: r1')) F i <=
\sum_(i <- (p1 ++ x :: p2)) F i
      rewrite big_cat 2!big_cons /= addnA [_ + F x]addnC -addnA leq_add2l.
I: eqType
r: seq I
P: pred I
F: I -> nat
x: I
r1': seq I
IH: forall rs : seq I,
{subset r1' <= rs} ->
\sum_(i <- r1') F i <= \sum_(i <- rs) F i
p1, p2: seq I
SUB: {subset x :: r1' <= p1 ++ x :: p2}
IN: x \in p1 ++ x :: p2
NOTIN: x \notin r1'
UNIQ: uniq r1'
\sum_(j <- r1') F j <=
\sum_(i <- p1) F i + \sum_(j <- p2) F j
      rewrite mem_cat in_cons eq_refl in IN.
I: eqType
r: seq I
P: pred I
F: I -> nat
x: I
r1': seq I
IH: forall rs : seq I,
{subset r1' <= rs} ->
\sum_(i <- r1') F i <= \sum_(i <- rs) F i
p1, p2: seq I
SUB: {subset x :: r1' <= p1 ++ x :: p2}
NOTIN: x \notin r1'
UNIQ: uniq r1'
IN: [|| x \in p1, true | x \in p2]
\sum_(j <- r1') F j <=
\sum_(i <- p1) F i + \sum_(j <- p2) F j
      rewrite -big_cat /=.
I: eqType
r: seq I
P: pred I
F: I -> nat
x: I
r1': seq I
IH: forall rs : seq I,
{subset r1' <= rs} ->
\sum_(i <- r1') F i <= \sum_(i <- rs) F i
p1, p2: seq I
SUB: {subset x :: r1' <= p1 ++ x :: p2}
NOTIN: x \notin r1'
UNIQ: uniq r1'
IN: [|| x \in p1, true | x \in p2]
\sum_(j <- r1') F j <= \sum_(i <- (p1 ++ p2)) F i
      apply IH; red; intros x0 IN0.
I: eqType
r: seq I
P: pred I
F: I -> nat
x: I
r1': seq I
IH: forall rs : seq I,
{subset r1' <= rs} ->
\sum_(i <- r1') F i <= \sum_(i <- rs) F i
p1, p2: seq I
SUB: {subset x :: r1' <= p1 ++ x :: p2}
NOTIN: x \notin r1'
UNIQ: uniq r1'
IN: [|| x \in p1, true | x \in p2]
x0: I
IN0: x0 \in r1'
x0 \in p1 ++ p2
      rewrite mem_cat.
I: eqType
r: seq I
P: pred I
F: I -> nat
x: I
r1': seq I
IH: forall rs : seq I,
{subset r1' <= rs} ->
\sum_(i <- r1') F i <= \sum_(i <- rs) F i
p1, p2: seq I
SUB: {subset x :: r1' <= p1 ++ x :: p2}
NOTIN: x \notin r1'
UNIQ: uniq r1'
IN: [|| x \in p1, true | x \in p2]
x0: I
IN0: x0 \in r1'
(x0 \in p1) || (x0 \in p2)
      feed (SUB x0); first by rewrite in_cons IN0 orbT.
I: eqType
r: seq I
P: pred I
F: I -> nat
x: I
r1': seq I
IH: forall rs : seq I,
{subset r1' <= rs} ->
\sum_(i <- r1') F i <= \sum_(i <- rs) F i
p1, p2: seq I
x0: I
SUB: x0 \in p1 ++ x :: p2
NOTIN: x \notin r1'
UNIQ: uniq r1'
IN: [|| x \in p1, true | x \in p2]
IN0: x0 \in r1'
(x0 \in p1) || (x0 \in p2)
      rewrite mem_cat in_cons in SUB.
I: eqType
r: seq I
P: pred I
F: I -> nat
x: I
r1': seq I
IH: forall rs : seq I,
{subset r1' <= rs} ->
\sum_(i <- r1') F i <= \sum_(i <- rs) F i
p1, p2: seq I
x0: I
NOTIN: x \notin r1'
UNIQ: uniq r1'
IN: [|| x \in p1, true | x \in p2]
IN0: x0 \in r1'
SUB: [|| x0 \in p1, x0 == x | x0 \in p2]
(x0 \in p1) || (x0 \in p2)
      move:SUB => /orP [SUB1 | /orP [/eqP EQx | SUB2]]; [by rewrite SUB1 | | by rewrite SUB2 orbT].
I: eqType
r: seq I
P: pred I
F: I -> nat
x: I
r1': seq I
IH: forall rs : seq I,
{subset r1' <= rs} ->
\sum_(i <- r1') F i <= \sum_(i <- rs) F i
p1, p2: seq I
x0: I
NOTIN: x \notin r1'
UNIQ: uniq r1'
IN: [|| x \in p1, true | x \in p2]
IN0: x0 \in r1'
EQx: x0 = x
(x0 \in p1) || (x0 \in p2)
      by rewrite -EQx IN0 in NOTIN.
    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
      intros LE.
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 | P i) E1 i <= \sum_(i <- r | P i) E2 i
      rewrite big_seq_cond [\sum_(_ <- _| P _)_]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
      by apply leq_sum; move => j /andP [IN H]; apply 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=> EQ.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
EQ: 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
      rewrite big_seq_cond [\sum_(_ <- _| P _)_]big_seq_cond.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
EQ: 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
      rewrite eqn_leq; apply /andP; split.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
EQ: 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
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
EQ: forall i : I, i \in r -> P i -> E1 i == E2 i
\sum_(i <- r | (i \in r) && P i) E2 i <=
\sum_(i <- r | (i \in r) && P i) E1 i
      all: apply leq_sum; move => j /andP [IN H].
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
EQ: forall i : I, i \in r -> P i -> E1 i == E2 i
j: I
IN: j \in r
H: P j
E1 j <= E2 j
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
EQ: forall i : I, i \in r -> P i -> E1 i == E2 i
j: I
IN: j \in r
H: P j
E2 j <= E1 j
      all: by move:(EQ j IN H) => LEQ; ssrlia.
    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
      intros LE.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
LE: forall i : I, i \in r -> P1 i -> P2 i
\sum_(i <- r | P1 i) E i <= \sum_(i <- r | P2 i) E i
      induction r; first by rewrite !big_nil.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LE: forall i : I, i \in a :: l -> P1 i -> P2 i
IHl: (forall i : I, i \in l -> P1 i -> P2 i) ->
\sum_(i <- l | P1 i) E i <= \sum_(i <- l | P2 i) E i
\sum_(i <- (a :: l) | P1 i) E i <=
\sum_(i <- (a :: l) | P2 i) E i
      rewrite !big_cons.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LE: forall i : I, i \in a :: l -> P1 i -> P2 i
IHl: (forall i : I, i \in l -> P1 i -> P2 i) ->
\sum_(i <- l | P1 i) E i <= \sum_(i <- l | P2 i) E i
(if P1 a
 then E a + \sum_(j <- l | P1 j) E j
 else \sum_(j <- l | P1 j) E j) <=
(if P2 a
 then E a + \sum_(j <- l | P2 j) E j
 else \sum_(j <- l | P2 j) E j)
      destruct (P1 a) eqn:P1a; first (move: P1a => /eqP; rewrite eqb_id => P1a).
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LE: forall i : I, i \in a :: l -> P1 i -> P2 i
IHl: (forall i : I, i \in l -> P1 i -> P2 i) ->
\sum_(i <- l | P1 i) E i <= \sum_(i <- l | P2 i) E i
P1a: P1 a
E a + \sum_(j <- l | P1 j) E j <=
(if P2 a
 then E a + \sum_(j <- l | P2 j) E j
 else \sum_(j <- l | P2 j) E j)
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LE: forall i : I, i \in a :: l -> P1 i -> P2 i
IHl: (forall i : I, i \in l -> P1 i -> P2 i) ->
\sum_(i <- l | P1 i) E i <= \sum_(i <- l | P2 i) E i
P1a: P1 a = false
\sum_(j <- l | P1 j) E j <=
(if P2 a
 then E a + \sum_(j <- l | P2 j) E j
 else \sum_(j <- l | P2 j) E j) 
      -
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LE: forall i : I, i \in a :: l -> P1 i -> P2 i
IHl: (forall i : I, i \in l -> P1 i -> P2 i) ->
\sum_(i <- l | P1 i) E i <= \sum_(i <- l | P2 i) E i
P1a: P1 a
E a + \sum_(j <- l | P1 j) E j <=
(if P2 a
 then E a + \sum_(j <- l | P2 j) E j
 else \sum_(j <- l | P2 j) E j)
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LE: forall i : I, i \in a :: l -> P1 i -> P2 i
IHl: (forall i : I, i \in l -> P1 i -> P2 i) ->
\sum_(i <- l | P1 i) E i <= \sum_(i <- l | P2 i) E i
P1a: P1 a = false
\sum_(j <- l | P1 j) E j <=
(if P2 a
 then E a + \sum_(j <- l | P2 j) E j
 else \sum_(j <- l | P2 j) E j) rewrite LE //; last by rewrite in_cons; apply/orP; left.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LE: forall i : I, i \in a :: l -> P1 i -> P2 i
IHl: (forall i : I, i \in l -> P1 i -> P2 i) ->
\sum_(i <- l | P1 i) E i <= \sum_(i <- l | P2 i) E i
P1a: P1 a
E a + \sum_(j <- l | P1 j) E j <=
E a + \sum_(j <- l | P2 j) E j
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LE: forall i : I, i \in a :: l -> P1 i -> P2 i
IHl: (forall i : I, i \in l -> P1 i -> P2 i) ->
\sum_(i <- l | P1 i) E i <= \sum_(i <- l | P2 i) E i
P1a: P1 a = false
\sum_(j <- l | P1 j) E j <=
(if P2 a
 then E a + \sum_(j <- l | P2 j) E j
 else \sum_(j <- l | P2 j) E j)
        rewrite leq_add2l.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LE: forall i : I, i \in a :: l -> P1 i -> P2 i
IHl: (forall i : I, i \in l -> P1 i -> P2 i) ->
\sum_(i <- l | P1 i) E i <= \sum_(i <- l | P2 i) E i
P1a: P1 a
\sum_(j <- l | P1 j) E j <= \sum_(j <- l | P2 j) E j
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LE: forall i : I, i \in a :: l -> P1 i -> P2 i
IHl: (forall i : I, i \in l -> P1 i -> P2 i) ->
\sum_(i <- l | P1 i) E i <= \sum_(i <- l | P2 i) E i
P1a: P1 a = false
\sum_(j <- l | P1 j) E j <=
(if P2 a
 then E a + \sum_(j <- l | P2 j) E j
 else \sum_(j <- l | P2 j) E j)
        by apply IHl; intros; apply LE => //; rewrite in_cons; apply/orP; right.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LE: forall i : I, i \in a :: l -> P1 i -> P2 i
IHl: (forall i : I, i \in l -> P1 i -> P2 i) ->
\sum_(i <- l | P1 i) E i <= \sum_(i <- l | P2 i) E i
P1a: P1 a = false
\sum_(j <- l | P1 j) E j <=
(if P2 a
 then E a + \sum_(j <- l | P2 j) E j
 else \sum_(j <- l | P2 j) E j)
      -
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LE: forall i : I, i \in a :: l -> P1 i -> P2 i
IHl: (forall i : I, i \in l -> P1 i -> P2 i) ->
\sum_(i <- l | P1 i) E i <= \sum_(i <- l | P2 i) E i
P1a: P1 a = false
\sum_(j <- l | P1 j) E j <=
(if P2 a
 then E a + \sum_(j <- l | P2 j) E j
 else \sum_(j <- l | P2 j) E j) destruct (P2 a) eqn:P2a.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LE: forall i : I, i \in a :: l -> P1 i -> P2 i
IHl: (forall i : I, i \in l -> P1 i -> P2 i) ->
\sum_(i <- l | P1 i) E i <= \sum_(i <- l | P2 i) E i
P1a: P1 a = false
P2a: P2 a = true
\sum_(j <- l | P1 j) E j <=
E a + \sum_(j <- l | P2 j) E j
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LE: forall i : I, i \in a :: l -> P1 i -> P2 i
IHl: (forall i : I, i \in l -> P1 i -> P2 i) ->
\sum_(i <- l | P1 i) E i <= \sum_(i <- l | P2 i) E i
P1a: P1 a = false
P2a: P2 a = false
\sum_(j <- l | P1 j) E j <= \sum_(j <- l | P2 j) E j
        +
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LE: forall i : I, i \in a :: l -> P1 i -> P2 i
IHl: (forall i : I, i \in l -> P1 i -> P2 i) ->
\sum_(i <- l | P1 i) E i <= \sum_(i <- l | P2 i) E i
P1a: P1 a = false
P2a: P2 a = true
\sum_(j <- l | P1 j) E j <=
E a + \sum_(j <- l | P2 j) E j
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LE: forall i : I, i \in a :: l -> P1 i -> P2 i
IHl: (forall i : I, i \in l -> P1 i -> P2 i) ->
\sum_(i <- l | P1 i) E i <= \sum_(i <- l | P2 i) E i
P1a: P1 a = false
P2a: P2 a = false
\sum_(j <- l | P1 j) E j <= \sum_(j <- l | P2 j) E j by eapply leq_trans;
            [apply IHl; intros; apply LE => //; rewrite in_cons; apply/orP; right
            | apply leq_addl].
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LE: forall i : I, i \in a :: l -> P1 i -> P2 i
IHl: (forall i : I, i \in l -> P1 i -> P2 i) ->
\sum_(i <- l | P1 i) E i <= \sum_(i <- l | P2 i) E i
P1a: P1 a = false
P2a: P2 a = false
\sum_(j <- l | P1 j) E j <= \sum_(j <- l | P2 j) E j
        +
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LE: forall i : I, i \in a :: l -> P1 i -> P2 i
IHl: (forall i : I, i \in l -> P1 i -> P2 i) ->
\sum_(i <- l | P1 i) E i <= \sum_(i <- l | P2 i) E i
P1a: P1 a = false
P2a: P2 a = false
\sum_(j <- l | P1 j) E j <= \sum_(j <- l | P2 j) E j by apply IHl; intros; apply LE => //; rewrite in_cons; apply/orP; right. 
    Qed.
    

    (** Next, we prove that if for any element x of a set [xs] the following two statements 
        hold (1) [F1 x] is less than or equal to [F2 x] and (2) the sum [F1 x_1, ..., F1 x_n] 
        is equal to the sum of [F2 x_1, ..., F2 x_n], then [F1 x] is equal to [F2 x] for 
        any element x of [xs]. *)
    Lemma sum_majorant_eqn:
      forall xs,
        (forall x, x \in xs -> P x -> E1 x <= E2 x) -> 
        \sum_(x <- xs | P x) E1 x = \sum_(x <- xs | P x) E2 x ->
        (forall x, x \in xs -> P x -> E1 x = E2 x).
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
forall xs : seq_predType I,
(forall x : I, x \in xs -> P x -> E1 x <= E2 x) ->
\sum_(x <- xs | P x) E1 x = \sum_(x <- xs | P x) E2 x ->
forall x : I, x \in xs -> P x -> E1 x = E2 x
    Proof.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
forall xs : seq_predType I,
(forall x : I, x \in xs -> P x -> E1 x <= E2 x) ->
\sum_(x <- xs | P x) E1 x = \sum_(x <- xs | P x) E2 x ->
forall x : I, x \in xs -> P x -> E1 x = E2 x
      intros xs H1 H2 x IN PX.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
xs: seq_predType I
H1: forall x : I, x \in xs -> P x -> E1 x <= E2 x
H2: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x
x: I
IN: x \in xs
PX: P x
E1 x = E2 x
      induction xs; first by done.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
H2: \sum_(x <- (a :: xs) | P x) E1 x =
\sum_(x <- (a :: xs) | P x) E2 x
x: I
IN: x \in a :: xs
PX: P x
IHxs: (forall x : I, x \in xs -> P x -> E1 x <= E2 x) ->
\sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
E1 x = E2 x
      have Fact: \sum_(j <- xs | P j) E1 j <= \sum_(j <- xs | P j) E2 j.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
H2: \sum_(x <- (a :: xs) | P x) E1 x =
\sum_(x <- (a :: xs) | P x) E2 x
x: I
IN: x \in a :: xs
PX: P x
IHxs: (forall x : I, x \in xs -> P x -> E1 x <= E2 x) ->
\sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
\sum_(j <- xs | P j) E1 j <= \sum_(j <- xs | P j) E2 j
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
H2: \sum_(x <- (a :: xs) | P x) E1 x =
\sum_(x <- (a :: xs) | P x) E2 x
x: I
IN: x \in a :: xs
PX: P x
IHxs: (forall x : I, x \in xs -> P x -> E1 x <= E2 x) ->
\sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
E1 x = E2 x
      {
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
H2: \sum_(x <- (a :: xs) | P x) E1 x =
\sum_(x <- (a :: xs) | P x) E2 x
x: I
IN: x \in a :: xs
PX: P x
IHxs: (forall x : I, x \in xs -> P x -> E1 x <= E2 x) ->
\sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
\sum_(j <- xs | P j) E1 j <= \sum_(j <- xs | P j) E2 j rewrite [in X in X <= _]big_seq_cond [in X in _ <= X]big_seq_cond leq_sum //.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
H2: \sum_(x <- (a :: xs) | P x) E1 x =
\sum_(x <- (a :: xs) | P x) E2 x
x: I
IN: x \in a :: xs
PX: P x
IHxs: (forall x : I, x \in xs -> P x -> E1 x <= E2 x) ->
\sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
forall i : I, (i \in xs) && P i -> E1 i <= E2 i
        move => y /andP [INy PY].
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
H2: \sum_(x <- (a :: xs) | P x) E1 x =
\sum_(x <- (a :: xs) | P x) E2 x
x: I
IN: x \in a :: xs
PX: P x
IHxs: (forall x : I, x \in xs -> P x -> E1 x <= E2 x) ->
\sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
y: I
INy: y \in xs
PY: P y
E1 y <= E2 y
        apply: H1; last by done.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H2: \sum_(x <- (a :: xs) | P x) E1 x =
\sum_(x <- (a :: xs) | P x) E2 x
x: I
IN: x \in a :: xs
PX: P x
IHxs: (forall x : I, x \in xs -> P x -> E1 x <= E2 x) ->
\sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
y: I
INy: y \in xs
PY: P y
y \in a :: xs 
        by rewrite in_cons; apply/orP; right. }
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
H2: \sum_(x <- (a :: xs) | P x) E1 x =
\sum_(x <- (a :: xs) | P x) E2 x
x: I
IN: x \in a :: xs
PX: P x
IHxs: (forall x : I, x \in xs -> P x -> E1 x <= E2 x) ->
\sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
E1 x = E2 x
      feed IHxs.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
H2: \sum_(x <- (a :: xs) | P x) E1 x =
\sum_(x <- (a :: xs) | P x) E2 x
x: I
IN: x \in a :: xs
PX: P x
IHxs: (forall x : I, x \in xs -> P x -> E1 x <= E2 x) ->
\sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
forall x : I, x \in xs -> P x -> E1 x <= E2 x
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
H2: \sum_(x <- (a :: xs) | P x) E1 x =
\sum_(x <- (a :: xs) | P x) E2 x
x: I
IN: x \in a :: xs
PX: P x
IHxs: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
E1 x = E2 x
      {
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
H2: \sum_(x <- (a :: xs) | P x) E1 x =
\sum_(x <- (a :: xs) | P x) E2 x
x: I
IN: x \in a :: xs
PX: P x
IHxs: (forall x : I, x \in xs -> P x -> E1 x <= E2 x) ->
\sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
forall x : I, x \in xs -> P x -> E1 x <= E2 x intros x' IN' PX'.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
H2: \sum_(x <- (a :: xs) | P x) E1 x =
\sum_(x <- (a :: xs) | P x) E2 x
x: I
IN: x \in a :: xs
PX: P x
IHxs: (forall x : I, x \in xs -> P x -> E1 x <= E2 x) ->
\sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
x': I
IN': x' \in xs
PX': P x'
E1 x' <= E2 x'
        apply H1; last by done.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
H2: \sum_(x <- (a :: xs) | P x) E1 x =
\sum_(x <- (a :: xs) | P x) E2 x
x: I
IN: x \in a :: xs
PX: P x
IHxs: (forall x : I, x \in xs -> P x -> E1 x <= E2 x) ->
\sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
x': I
IN': x' \in xs
PX': P x'
x' \in a :: xs
        by rewrite in_cons; apply/orP; right. }
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
H2: \sum_(x <- (a :: xs) | P x) E1 x =
\sum_(x <- (a :: xs) | P x) E2 x
x: I
IN: x \in a :: xs
PX: P x
IHxs: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
E1 x = E2 x
      rewrite big_cons [RHS]big_cons in H2.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
x: I
IN: x \in a :: xs
PX: P x
IHxs: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
H2: (if P a
 then E1 a + \sum_(j <- xs | P j) E1 j
 else \sum_(j <- xs | P j) E1 j) =
(if P a
 then E2 a + \sum_(j <- xs | P j) E2 j
 else \sum_(j <- xs | P j) E2 j)
E1 x = E2 x
      have EqLeq: forall a b c d, a + b = c + d -> a <= c -> b >= d by intros; ssrlia.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
x: I
IN: x \in a :: xs
PX: P x
IHxs: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
H2: (if P a
 then E1 a + \sum_(j <- xs | P j) E1 j
 else \sum_(j <- xs | P j) E1 j) =
(if P a
 then E2 a + \sum_(j <- xs | P j) E2 j
 else \sum_(j <- xs | P j) E2 j)
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
E1 x = E2 x
      move: IN; rewrite in_cons; move => /orP [/eqP EQ | IN].
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
x: I
PX: P x
IHxs: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
H2: (if P a
 then E1 a + \sum_(j <- xs | P j) E1 j
 else \sum_(j <- xs | P j) E1 j) =
(if P a
 then E2 a + \sum_(j <- xs | P j) E2 j
 else \sum_(j <- xs | P j) E2 j)
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
EQ: x = a
E1 x = E2 x
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
x: I
PX: P x
IHxs: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
H2: (if P a
 then E1 a + \sum_(j <- xs | P j) E1 j
 else \sum_(j <- xs | P j) E1 j) =
(if P a
 then E2 a + \sum_(j <- xs | P j) E2 j
 else \sum_(j <- xs | P j) E2 j)
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
IN: x \in xs
E1 x = E2 x 
      {
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
x: I
PX: P x
IHxs: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
H2: (if P a
 then E1 a + \sum_(j <- xs | P j) E1 j
 else \sum_(j <- xs | P j) E1 j) =
(if P a
 then E2 a + \sum_(j <- xs | P j) E2 j
 else \sum_(j <- xs | P j) E2 j)
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
EQ: x = a
E1 x = E2 x subst a.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
xs: seq I
x: I
H1: forall x0 : I,
x0 \in x :: xs -> P x0 -> E1 x0 <= E2 x0
PX: P x
IHxs: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
H2: (if P x
 then E1 x + \sum_(j <- xs | P j) E1 j
 else \sum_(j <- xs | P j) E1 j) =
(if P x
 then E2 x + \sum_(j <- xs | P j) E2 j
 else \sum_(j <- xs | P j) E2 j)
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
E1 x = E2 x
        rewrite PX in H2.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
xs: seq I
x: I
H1: forall x0 : I,
x0 \in x :: xs -> P x0 -> E1 x0 <= E2 x0
PX: P x
IHxs: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
H2: E1 x + \sum_(j <- xs | P j) E1 j =
E2 x + \sum_(j <- xs | P j) E2 j
E1 x = E2 x
        specialize (H1 x).
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
xs: seq I
x: I
H1: x \in x :: xs -> P x -> E1 x <= E2 x
PX: P x
IHxs: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
H2: E1 x + \sum_(j <- xs | P j) E1 j =
E2 x + \sum_(j <- xs | P j) E2 j
E1 x = E2 x
        feed_n 2 H1=> //; first by rewrite in_cons; apply/orP; left.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
xs: seq I
x: I
H1: E1 x <= E2 x
PX: P x
IHxs: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
H2: E1 x + \sum_(j <- xs | P j) E1 j =
E2 x + \sum_(j <- xs | P j) E2 j
E1 x = E2 x
        move: (EqLeq
                 (E1 x) (\sum_(j <- xs | P j) E1 j)
                 (E2 x) (\sum_(j <- xs | P j) E2 j) H2 H1) => Q.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
xs: seq I
x: I
H1: E1 x <= E2 x
PX: P x
IHxs: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
H2: E1 x + \sum_(j <- xs | P j) E1 j =
E2 x + \sum_(j <- xs | P j) E2 j
Q: \sum_(j <- xs | P j) E2 j <=
\sum_(j <- xs | P j) E1 j
E1 x = E2 x
        have EQ: \sum_(j <- xs | P j) E1 j = \sum_(j <- xs | P j) E2 j.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
xs: seq I
x: I
H1: E1 x <= E2 x
PX: P x
IHxs: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
H2: E1 x + \sum_(j <- xs | P j) E1 j =
E2 x + \sum_(j <- xs | P j) E2 j
Q: \sum_(j <- xs | P j) E2 j <=
\sum_(j <- xs | P j) E1 j
\sum_(j <- xs | P j) E1 j = \sum_(j <- xs | P j) E2 j
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
xs: seq I
x: I
H1: E1 x <= E2 x
PX: P x
IHxs: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
H2: E1 x + \sum_(j <- xs | P j) E1 j =
E2 x + \sum_(j <- xs | P j) E2 j
Q: \sum_(j <- xs | P j) E2 j <=
\sum_(j <- xs | P j) E1 j
EQ: \sum_(j <- xs | P j) E1 j =
\sum_(j <- xs | P j) E2 j
E1 x = E2 x 
        {
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
xs: seq I
x: I
H1: E1 x <= E2 x
PX: P x
IHxs: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
H2: E1 x + \sum_(j <- xs | P j) E1 j =
E2 x + \sum_(j <- xs | P j) E2 j
Q: \sum_(j <- xs | P j) E2 j <=
\sum_(j <- xs | P j) E1 j
\sum_(j <- xs | P j) E1 j = \sum_(j <- xs | P j) E2 j by apply /eqP; rewrite eqn_leq; apply/andP; split. }
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
xs: seq I
x: I
H1: E1 x <= E2 x
PX: P x
IHxs: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
H2: E1 x + \sum_(j <- xs | P j) E1 j =
E2 x + \sum_(j <- xs | P j) E2 j
Q: \sum_(j <- xs | P j) E2 j <=
\sum_(j <- xs | P j) E1 j
EQ: \sum_(j <- xs | P j) E1 j =
\sum_(j <- xs | P j) E2 j
E1 x = E2 x
        by move: H2 => /eqP; rewrite EQ eqn_add2r; move => /eqP EQ'. }
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
x: I
PX: P x
IHxs: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
H2: (if P a
 then E1 a + \sum_(j <- xs | P j) E1 j
 else \sum_(j <- xs | P j) E1 j) =
(if P a
 then E2 a + \sum_(j <- xs | P j) E2 j
 else \sum_(j <- xs | P j) E2 j)
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
IN: x \in xs
E1 x = E2 x
      {
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
x: I
PX: P x
IHxs: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
H2: (if P a
 then E1 a + \sum_(j <- xs | P j) E1 j
 else \sum_(j <- xs | P j) E1 j) =
(if P a
 then E2 a + \sum_(j <- xs | P j) E2 j
 else \sum_(j <- xs | P j) E2 j)
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
IN: x \in xs
E1 x = E2 x destruct (P a) eqn:PA; last by apply IHxs.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
x: I
PX: P x
IHxs: \sum_(x <- xs | P x) E1 x =
\sum_(x <- xs | P x) E2 x ->
x \in xs -> E1 x = E2 x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
PA: P a = true
H2: E1 a + \sum_(j <- xs | P j) E1 j =
E2 a + \sum_(j <- xs | P j) E2 j
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
IN: x \in xs
E1 x = E2 x
        apply: IHxs; last by done.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: forall x : I,
x \in a :: xs -> P x -> E1 x <= E2 x
x: I
PX: P x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
PA: P a = true
H2: E1 a + \sum_(j <- xs | P j) E1 j =
E2 a + \sum_(j <- xs | P j) E2 j
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
IN: x \in xs
\sum_(x <- xs | P x) E1 x = \sum_(x <- xs | P x) E2 x
        specialize (H1 a).
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: a \in a :: xs -> P a -> E1 a <= E2 a
x: I
PX: P x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
PA: P a = true
H2: E1 a + \sum_(j <- xs | P j) E1 j =
E2 a + \sum_(j <- xs | P j) E2 j
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
IN: x \in xs
\sum_(x <- xs | P x) E1 x = \sum_(x <- xs | P x) E2 x
        feed_n 2 (H1); [ by rewrite in_cons; apply/orP; left | by done | ].
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: E1 a <= E2 a
x: I
PX: P x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
PA: P a = true
H2: E1 a + \sum_(j <- xs | P j) E1 j =
E2 a + \sum_(j <- xs | P j) E2 j
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
IN: x \in xs
\sum_(x <- xs | P x) E1 x = \sum_(x <- xs | P x) E2 x
        move: (EqLeq
                 (E1 a) (\sum_(j <- xs | P j) E1 j)
                 (E2 a) (\sum_(j <- xs | P j) E2 j) H2 H1) => Q.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
xs: seq I
H1: E1 a <= E2 a
x: I
PX: P x
Fact: \sum_(j <- xs | P j) E1 j <=
\sum_(j <- xs | P j) E2 j
PA: P a = true
H2: E1 a + \sum_(j <- xs | P j) E1 j =
E2 a + \sum_(j <- xs | P j) E2 j
EqLeq: forall a b c d : nat,
a + b = c + d -> a <= c -> d <= b
IN: x \in xs
Q: \sum_(j <- xs | P j) E2 j <=
\sum_(j <- xs | P j) E1 j
\sum_(x <- xs | P x) E1 x = \sum_(x <- xs | P x) E2 x
        by apply/eqP; rewrite eqn_leq; apply/andP; split. }
    Qed.

    (** Next, we prove that the summing over the difference of [E1] and [E2] is
        the same as the difference of the two sums performed separately. Since we
        are using natural numbers, we have to require that [E2] dominates [E1] over
        the summing points given by [r]. *)
    Lemma sum_seq_diff:
        (forall i : I, i \in r -> E1 i <= E2 i) ->
        \sum_(i <- r) (E2 i - E1 i) = \sum_(i <- r) E2 i - \sum_(i <- r) E1 i.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
(forall i : I, i \in r -> E1 i <= E2 i) ->
\sum_(i <- r) (E2 i - E1 i) =
\sum_(i <- r) E2 i - \sum_(i <- r) E1 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 -> E1 i <= E2 i) ->
\sum_(i <- r) (E2 i - E1 i) =
\sum_(i <- r) E2 i - \sum_(i <- r) E1 i
      move=> LEQ.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
LEQ: forall i : I, i \in r -> E1 i <= E2 i
\sum_(i <- r) (E2 i - E1 i) =
\sum_(i <- r) E2 i - \sum_(i <- r) E1 i
      induction r; first by rewrite !big_nil subn0.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LEQ: forall i : I, i \in a :: l -> E1 i <= E2 i
IHl: (forall i : I, i \in l -> E1 i <= E2 i) ->
\sum_(i <- l) (E2 i - E1 i) = \sum_(i <- l) E2 i - \sum_(i <- l) E1 i
\sum_(i <- (a :: l)) (E2 i - E1 i) =
\sum_(i <- (a :: l)) E2 i - \sum_(i <- (a :: l)) E1 i 
      rewrite !big_cons subnD.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LEQ: forall i : I, i \in a :: l -> E1 i <= E2 i
IHl: (forall i : I, i \in l -> E1 i <= E2 i) ->
\sum_(i <- l) (E2 i - E1 i) = \sum_(i <- l) E2 i - \sum_(i <- l) E1 i
E2 a - E1 a + \sum_(j <- l) (E2 j - E1 j) =
E2 a - E1 a +
(\sum_(j <- l) E2 j - \sum_(j <- l) E1 j)
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LEQ: forall i : I, i \in a :: l -> E1 i <= E2 i
IHl: (forall i : I, i \in l -> E1 i <= E2 i) ->
\sum_(i <- l) (E2 i - E1 i) = \sum_(i <- l) E2 i - \sum_(i <- l) E1 i
E1 a <= E2 a
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LEQ: forall i : I, i \in a :: l -> E1 i <= E2 i
IHl: (forall i : I, i \in l -> E1 i <= E2 i) ->
\sum_(i <- l) (E2 i - E1 i) = \sum_(i <- l) E2 i - \sum_(i <- l) E1 i
\sum_(j <- l) E1 j <= \sum_(j <- l) E2 j
      -
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LEQ: forall i : I, i \in a :: l -> E1 i <= E2 i
IHl: (forall i : I, i \in l -> E1 i <= E2 i) ->
\sum_(i <- l) (E2 i - E1 i) = \sum_(i <- l) E2 i - \sum_(i <- l) E1 i
E2 a - E1 a + \sum_(j <- l) (E2 j - E1 j) =
E2 a - E1 a +
(\sum_(j <- l) E2 j - \sum_(j <- l) E1 j)
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LEQ: forall i : I, i \in a :: l -> E1 i <= E2 i
IHl: (forall i : I, i \in l -> E1 i <= E2 i) ->
\sum_(i <- l) (E2 i - E1 i) = \sum_(i <- l) E2 i - \sum_(i <- l) E1 i
E1 a <= E2 a
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LEQ: forall i : I, i \in a :: l -> E1 i <= E2 i
IHl: (forall i : I, i \in l -> E1 i <= E2 i) ->
\sum_(i <- l) (E2 i - E1 i) = \sum_(i <- l) E2 i - \sum_(i <- l) E1 i
\sum_(j <- l) E1 j <= \sum_(j <- l) E2 j apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHl.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LEQ: forall i : I, i \in a :: l -> E1 i <= E2 i
IHl: (forall i : I, i \in l -> E1 i <= E2 i) ->
\sum_(i <- l) (E2 i - E1 i) = \sum_(i <- l) E2 i - \sum_(i <- l) E1 i
forall i : I, i \in l -> E1 i <= E2 i
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LEQ: forall i : I, i \in a :: l -> E1 i <= E2 i
IHl: (forall i : I, i \in l -> E1 i <= E2 i) ->
\sum_(i <- l) (E2 i - E1 i) = \sum_(i <- l) E2 i - \sum_(i <- l) E1 i
E1 a <= E2 a
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LEQ: forall i : I, i \in a :: l -> E1 i <= E2 i
IHl: (forall i : I, i \in l -> E1 i <= E2 i) ->
\sum_(i <- l) (E2 i - E1 i) = \sum_(i <- l) E2 i - \sum_(i <- l) E1 i
\sum_(j <- l) E1 j <= \sum_(j <- l) E2 j
        by intros; apply LEQ; rewrite in_cons; apply/orP; right.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LEQ: forall i : I, i \in a :: l -> E1 i <= E2 i
IHl: (forall i : I, i \in l -> E1 i <= E2 i) ->
\sum_(i <- l) (E2 i - E1 i) = \sum_(i <- l) E2 i - \sum_(i <- l) E1 i
E1 a <= E2 a
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LEQ: forall i : I, i \in a :: l -> E1 i <= E2 i
IHl: (forall i : I, i \in l -> E1 i <= E2 i) ->
\sum_(i <- l) (E2 i - E1 i) = \sum_(i <- l) E2 i - \sum_(i <- l) E1 i
\sum_(j <- l) E1 j <= \sum_(j <- l) E2 j
      -
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LEQ: forall i : I, i \in a :: l -> E1 i <= E2 i
IHl: (forall i : I, i \in l -> E1 i <= E2 i) ->
\sum_(i <- l) (E2 i - E1 i) = \sum_(i <- l) E2 i - \sum_(i <- l) E1 i
E1 a <= E2 a
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LEQ: forall i : I, i \in a :: l -> E1 i <= E2 i
IHl: (forall i : I, i \in l -> E1 i <= E2 i) ->
\sum_(i <- l) (E2 i - E1 i) = \sum_(i <- l) E2 i - \sum_(i <- l) E1 i
\sum_(j <- l) E1 j <= \sum_(j <- l) E2 j by apply LEQ; rewrite in_cons; apply/orP; left.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LEQ: forall i : I, i \in a :: l -> E1 i <= E2 i
IHl: (forall i : I, i \in l -> E1 i <= E2 i) ->
\sum_(i <- l) (E2 i - E1 i) = \sum_(i <- l) E2 i - \sum_(i <- l) E1 i
\sum_(j <- l) E1 j <= \sum_(j <- l) E2 j
      -
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LEQ: forall i : I, i \in a :: l -> E1 i <= E2 i
IHl: (forall i : I, i \in l -> E1 i <= E2 i) ->
\sum_(i <- l) (E2 i - E1 i) = \sum_(i <- l) E2 i - \sum_(i <- l) E1 i
\sum_(j <- l) E1 j <= \sum_(j <- l) E2 j rewrite big_seq_cond [in X in _ <= X]big_seq_cond.
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LEQ: forall i : I, i \in a :: l -> E1 i <= E2 i
IHl: (forall i : I, i \in l -> E1 i <= E2 i) ->
\sum_(i <- l) (E2 i - E1 i) = \sum_(i <- l) E2 i - \sum_(i <- l) E1 i
\sum_(i <- l | (i \in l) && true) E1 i <=
\sum_(i <- l | (i \in l) && true) E2 i
        rewrite leq_sum //; move => i /andP [IN _].
I: eqType
r: seq I
P: pred I
E, E1, E2: I -> nat
P1, P2: pred I
a: I
l: seq I
LEQ: forall i : I, i \in a :: l -> E1 i <= E2 i
IHl: (forall i : I, i \in l -> E1 i <= E2 i) ->
\sum_(i <- l) (E2 i - E1 i) = \sum_(i <- l) E2 i - \sum_(i <- l) E1 i
i: I
IN: i \in l
E1 i <= E2 i
        by apply LEQ; rewrite in_cons; apply/orP; right.
    Qed.

  End SumOfTwoFunctions.
  
End SumsOverSequences.

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

  (** First, we show a trivial identity: any sum of zeros is zero. *)
  Lemma sum0 m n:
    \sum_(m <= i < n) 0 = 0.
m, n: nat
\sum_(m <= i < n) 0 = 0
  Proof.
m, n: nat
\sum_(m <= i < n) 0 = 0
    by rewrite big_const_nat iter_addn mul0n addn0 //.
  Qed.
  
  (** In a similar way, 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 = Δ
    move=> t Δ.
t, Δ: nat
\sum_(t <= x < t + Δ) 1 = Δ
    rewrite big_const_nat iter_addn_0.
t, Δ: nat
1 * (t + Δ - t) = Δ
    by ssrlia.
  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 => /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
      by apply sum0.
  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 sum_diff:
    forall n F G,
      (forall i, i < n -> F i >= G i) ->
      \sum_(0 <= i < n) (F i - G i) =
      (\sum_(0 <= i < n) (F i)) - (\sum_(0 <= i < n) (G i)).
forall (n : nat) (F G : nat -> nat),
(forall i : nat, i < n -> G i <= F i) ->
\sum_(0 <= i < n) (F i - G i) =
\sum_(0 <= i < n) F i - \sum_(0 <= i < n) G i       
  Proof.
forall (n : nat) (F G : nat -> nat),
(forall i : nat, i < n -> G i <= F i) ->
\sum_(0 <= i < n) (F i - G i) =
\sum_(0 <= i < n) F i - \sum_(0 <= i < n) G i
    intros n F G ALL.
n: nat
F, G: nat -> nat
ALL: forall i : nat, i < n -> G i <= F i
\sum_(0 <= i < n) (F i - G i) =
\sum_(0 <= i < n) F i - \sum_(0 <= i < n) G i
    rewrite sum_seq_diff; first by done.
n: nat
F, G: nat -> nat
ALL: forall i : nat, i < n -> G i <= F i
forall i : nat_eqType,
i \in index_iota 0 n -> G i <= F i
    move=> i; rewrite mem_index_iota; move => /andP [_ LT].
n: nat
F, G: nat -> nat
ALL: forall i : nat, i < n -> G i <= F i
i: nat_eqType
LT: i < n
G i <= F i
    by apply ALL.
  Qed.

  (** Given a sequence [r], function [F], and a predicate [P], we
      prove that the fact that the sum of [F] conditioned by [P] is
      greater than [0] is equivalent to the fact that there exists an
      element [i \in r] such that [F i > 0] and [P i] holds. *) 
  Lemma sum_seq_cond_gt0P:
    forall (T : eqType) (r : seq T) (P : T -> bool) (F : T -> nat),
      reflect (exists i, i \in r /\ P i /\ 0 < F i) (0 < \sum_(i <- r | P i) F i).
forall (T : eqType) (r : seq T) (P : T -> bool)
  (F : T -> nat),
reflect (exists i : T, i \in r /\ P i /\ 0 < F i)
  (0 < \sum_(i <- r | P i) F i)
  Proof.
forall (T : eqType) (r : seq T) (P : T -> bool)
  (F : T -> nat),
reflect (exists i : T, i \in r /\ P i /\ 0 < F i)
  (0 < \sum_(i <- r | P i) F i)
    intros; apply: (iffP idP); intros.
T: eqType
r: seq T
P: T -> bool
F: T -> nat
H: 0 < \sum_(i <- r | P i) F i
exists i : T, i \in r /\ P i /\ 0 < F i
T: eqType
r: seq T
P: T -> bool
F: T -> nat
H: exists i : T, i \in r /\ P i /\ 0 < F i
0 < \sum_(i <- r | P i) F i
    {
T: eqType
r: seq T
P: T -> bool
F: T -> nat
H: 0 < \sum_(i <- r | P i) F i
exists i : T, i \in r /\ P i /\ 0 < F i induction r; first by rewrite big_nil in H.
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
H: 0 < \sum_(i <- (a :: r) | P i) F i
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
exists i : T, i \in a :: r /\ P i /\ 0 < F i
      rewrite big_cons in H.
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
H: 0 <
(if P a
 then F a + \sum_(j <- r | P j) F j
 else \sum_(j <- r | P j) F j)
exists i : T, i \in a :: r /\ P i /\ 0 < F i
      destruct (P a) eqn:PA, (F a > 0) eqn:POS.
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = true
H: 0 < F a + \sum_(j <- r | P j) F j
POS: (0 < F a) = true
exists i : T, i \in a :: r /\ P i /\ 0 < F i
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = true
H: 0 < F a + \sum_(j <- r | P j) F j
POS: (0 < F a) = false
exists i : T, i \in a :: r /\ P i /\ 0 < F i
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
H: 0 < \sum_(j <- r | P j) F j
POS: (0 < F a) = true
exists i : T, i \in a :: r /\ P i /\ 0 < F i
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
H: 0 < \sum_(j <- r | P j) F j
POS: (0 < F a) = false
exists i : T, i \in a :: r /\ P i /\ 0 < F i
      -
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = true
H: 0 < F a + \sum_(j <- r | P j) F j
POS: (0 < F a) = true
exists i : T, i \in a :: r /\ P i /\ 0 < F i
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = true
H: 0 < F a + \sum_(j <- r | P j) F j
POS: (0 < F a) = false
exists i : T, i \in a :: r /\ P i /\ 0 < F i
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
H: 0 < \sum_(j <- r | P j) F j
POS: (0 < F a) = true
exists i : T, i \in a :: r /\ P i /\ 0 < F i
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
H: 0 < \sum_(j <- r | P j) F j
POS: (0 < F a) = false
exists i : T, i \in a :: r /\ P i /\ 0 < F i exists a; repeat split; [by rewrite in_cons; apply/orP; left | by done | by done].
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = true
H: 0 < F a + \sum_(j <- r | P j) F j
POS: (0 < F a) = false
exists i : T, i \in a :: r /\ P i /\ 0 < F i
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
H: 0 < \sum_(j <- r | P j) F j
POS: (0 < F a) = true
exists i : T, i \in a :: r /\ P i /\ 0 < F i
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
H: 0 < \sum_(j <- r | P j) F j
POS: (0 < F a) = false
exists i : T, i \in a :: r /\ P i /\ 0 < F i
      -
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = true
H: 0 < F a + \sum_(j <- r | P j) F j
POS: (0 < F a) = false
exists i : T, i \in a :: r /\ P i /\ 0 < F i
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
H: 0 < \sum_(j <- r | P j) F j
POS: (0 < F a) = true
exists i : T, i \in a :: r /\ P i /\ 0 < F i
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
H: 0 < \sum_(j <- r | P j) F j
POS: (0 < F a) = false
exists i : T, i \in a :: r /\ P i /\ 0 < F i move: POS => /negP/negP; rewrite -leqNgt leqn0 => /eqP Z; rewrite Z add0n in H.
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = true
Z: F a = 0
H: 0 < \sum_(j <- r | P j) F j
exists i : T, i \in a :: r /\ P i /\ 0 < F i
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
H: 0 < \sum_(j <- r | P j) F j
POS: (0 < F a) = true
exists i : T, i \in a :: r /\ P i /\ 0 < F i
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
H: 0 < \sum_(j <- r | P j) F j
POS: (0 < F a) = false
exists i : T, i \in a :: r /\ P i /\ 0 < F i
        apply IHr in H; destruct H as [i [IN [Pi POS]]].
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = true
Z: F a = 0
i: T
IN: i \in r
Pi: P i
POS: 0 < F i
exists i : T, i \in a :: r /\ P i /\ 0 < F i
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
H: 0 < \sum_(j <- r | P j) F j
POS: (0 < F a) = true
exists i : T, i \in a :: r /\ P i /\ 0 < F i
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
H: 0 < \sum_(j <- r | P j) F j
POS: (0 < F a) = false
exists i : T, i \in a :: r /\ P i /\ 0 < F i
        by (exists i; repeat split; [rewrite in_cons;apply/orP;right | | ]).
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
H: 0 < \sum_(j <- r | P j) F j
POS: (0 < F a) = true
exists i : T, i \in a :: r /\ P i /\ 0 < F i
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
H: 0 < \sum_(j <- r | P j) F j
POS: (0 < F a) = false
exists i : T, i \in a :: r /\ P i /\ 0 < F i
      -
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
H: 0 < \sum_(j <- r | P j) F j
POS: (0 < F a) = true
exists i : T, i \in a :: r /\ P i /\ 0 < F i
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
H: 0 < \sum_(j <- r | P j) F j
POS: (0 < F a) = false
exists i : T, i \in a :: r /\ P i /\ 0 < F i clear POS; apply IHr in H; destruct H as [i [IN [Pi POS]]].
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
i: T
IN: i \in r
Pi: P i
POS: 0 < F i
exists i : T, i \in a :: r /\ P i /\ 0 < F i
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
H: 0 < \sum_(j <- r | P j) F j
POS: (0 < F a) = false
exists i : T, i \in a :: r /\ P i /\ 0 < F i
        by (exists i; repeat split; [rewrite in_cons;apply/orP;right | | ]).
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
H: 0 < \sum_(j <- r | P j) F j
POS: (0 < F a) = false
exists i : T, i \in a :: r /\ P i /\ 0 < F i
      -
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
H: 0 < \sum_(j <- r | P j) F j
POS: (0 < F a) = false
exists i : T, i \in a :: r /\ P i /\ 0 < F i clear POS; apply IHr in H; destruct H as [i [IN [Pi POS]]].
T: eqType
a: T
r: seq T
P: T -> bool
F: T -> nat
IHr: 0 < \sum_(i <- r | P i) F i -> exists i : T, i \in r /\ P i /\ 0 < F i
PA: P a = false
i: T
IN: i \in r
Pi: P i
POS: 0 < F i
exists i : T, i \in a :: r /\ P i /\ 0 < F i
        by (exists i; repeat split; [rewrite in_cons;apply/orP;right | | ]).
    }
T: eqType
r: seq T
P: T -> bool
F: T -> nat
H: exists i : T, i \in r /\ P i /\ 0 < F i
0 < \sum_(i <- r | P i) F i
    {
T: eqType
r: seq T
P: T -> bool
F: T -> nat
H: exists i : T, i \in r /\ P i /\ 0 < F i
0 < \sum_(i <- r | P i) F i move: H => [i [IN [Pi POS]]].
T: eqType
r: seq T
P: T -> bool
F: T -> nat
i: T
IN: i \in r
Pi: P i
POS: 0 < F i
0 < \sum_(i <- r | P i) F i
      rewrite (big_rem i) //=; rewrite Pi.
T: eqType
r: seq T
P: T -> bool
F: T -> nat
i: T
IN: i \in r
Pi: P i
POS: 0 < F i
0 < F i + \sum_(y <- rem (T:=T) i r | P y) F y      
      by apply leq_trans with (F i); last rewrite leq_addr.
    }
  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 ssrlia.
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); ssrlia.
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.

  (** 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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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.