Library prosa.util.sum


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

Welcome to Coq 8.13.0 (January 2021)

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

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

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.

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

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

1 subgoal (ID 26)
  
  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.
      destruct (all (fun x ⇒ F x == 0) r) eqn:ZERO.

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

2 subgoals (ID 41)
  
  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)

subgoal 2 (ID 42) is:
 false = (\sum_(i <- r) F i == 0)

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

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

1 subgoal (ID 41)
  
  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.

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

1 subgoal (ID 80)
  
  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.

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

1 subgoal (ID 109)
  
  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.

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

1 subgoal (ID 130)
  
  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.

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

1 subgoal (ID 148)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 42) is:
 false = (\sum_(i <- r) F i == 0)

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

}

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

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

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

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

1 subgoal (ID 42)
  
  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.

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

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

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

1 subgoal (ID 322)
  
  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) //=.

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

1 subgoal (ID 339)
  
  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.

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

1 subgoal (ID 394)
  
  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.

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

1 subgoal (ID 395)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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

}

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

No more subgoals.

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

    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 (∃ i, i \in r ∧ 0 < F i) (0 < \sum_(i <- r) F i).

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

1 subgoal (ID 39)
  
  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.
      apply: (iffP idP); move⇒ LT0.

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

2 subgoals (ID 73)
  
  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

subgoal 2 (ID 74) is:
 0 < \sum_(i <- r) F i

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

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

1 subgoal (ID 73)
  
  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.

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

1 subgoal (ID 91)
  
  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.

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

2 subgoals (ID 147)
  
  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

subgoal 2 (ID 148) is:
 exists i : I, i \in a :: l /\ 0 < F i

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

        - ∃ a.

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

2 subgoals (ID 150)
  
  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

subgoal 2 (ID 148) is:
 exists i : I, i \in a :: l /\ 0 < F i

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

          by split ⇒ //; rewrite in_cons; apply /orP; left.

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

1 subgoal (ID 148)
  
  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.

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

1 subgoal (ID 266)
  
  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.

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

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

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

1 subgoal (ID 321)
  
  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 i0 : I, i0 \in a :: l /\ 0 < F i0

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

          by ∃ i; split ⇒ //; rewrite in_cons; apply /orP; right.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 74) is:
 0 < \sum_(i <- r) F i

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

}

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

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

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

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

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

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

1 subgoal (ID 402)
  
  I : eqType
  r : seq I
  P : pred I
  F : I -> nat
  i : I
  IN : i \in r
  POS : 0 < F i
  ============================
  0 < \sum_(i0 <- r) F i0

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

        rewrite (big_rem i) //=.

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

1 subgoal (ID 419)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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

}

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

No more subgoals.

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

    Qed.

Next, we show that if a number [a] is not contained in [r], then filtering or not filtering [a] when summing leads to the same result.
    Lemma sum_notin_rem_eqn:
      ∀ a,
        a \notin r →
        \sum_(x <- r | P x && (x != a)) F x = \sum_(x <- r | P x) F x.

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

1 subgoal (ID 58)
  
  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.
      intros a NOTIN.

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

1 subgoal (ID 60)
  
  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.

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

1 subgoal (ID 77)
  
  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.

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

2 subgoals (ID 130)
  
  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)

subgoal 2 (ID 131) is:
 a \notin l

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

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

1 subgoal (ID 130)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 166)
  
  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.

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

1 subgoal (ID 168)
  
  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).

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

1 subgoal (ID 174)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 131) is:
 a \notin l

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

}

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

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

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

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

1 subgoal (ID 131)
  
  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.

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

1 subgoal (ID 242)
  
  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.

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

1 subgoal (ID 277)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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

}

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

No more subgoals.

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

    Qed.

We prove that if any element of [r] is bounded by constant [c], then the sum of the whole set is bounded by [c * size r].
    Lemma sum_majorant_constant:
      ∀ c,
        (∀ a, a \in r → P a → F a ≤ c) →
        \sum_(j <- r | P j) F j ≤ c × (size [seq j <- r | P j]).

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

1 subgoal (ID 74)
  
  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.
      intros.

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

1 subgoal (ID 76)
  
  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.

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

1 subgoal (ID 93)
  
  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.

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

2 subgoals (ID 102)
  
  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 a0 : I, a0 \in l -> P a0 -> F a0 <= c

subgoal 2 (ID 107) is:
 \sum_(j <- (a :: l) | P j) F j <= c * size [seq j <- a :: l | P j]

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

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

1 subgoal (ID 102)
  
  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 a0 : I, a0 \in l -> P a0 -> F a0 <= c

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

intros; apply H.

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

2 subgoals (ID 111)
  
  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

subgoal 2 (ID 112) is:
 P a0

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

        - by rewrite in_cons; apply/orP; right.

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

1 subgoal (ID 112)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 107) is:
 \sum_(j <- (a :: l) | P j) F j <= c * size [seq j <- a :: l | P j]

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

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

1 subgoal (ID 107)
  
  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.

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

1 subgoal (ID 154)
  
  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.

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

2 subgoals (ID 166)
  
  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]

subgoal 2 (ID 167) is:
 \sum_(j <- l | P j) F j <= c * size [seq j <- a :: l | P j]

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

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

1 subgoal (ID 166)
  
  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.

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

1 subgoal (ID 191)
  
  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.

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

1 subgoal (ID 192)
  
  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.

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

1 subgoal (ID 234)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 235)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 167) is:
 \sum_(j <- l | P j) F j <= c * size [seq j <- a :: l | P j]

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

}

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

1 subgoal (ID 167)
  
  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]

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

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

1 subgoal (ID 167)
  
  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.

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

1 subgoal (ID 273)
  
  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.

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

1 subgoal (ID 304)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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

}

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

No more subgoals.

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

    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.

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

1 subgoal (ID 91)
  
  I : eqType
  r : seq I
  P : pred I
  F : I -> nat
  ============================
  \sum_(r0 <- r | P r0) F r0 =
  \sum_(r0 <- r) F r0 - \sum_(r0 <- r | ~~ P r0) F r0

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

    Proof.
      induction r; first by rewrite !big_nil subn0.

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

1 subgoal (ID 102)
  
  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_(r0 <- (a :: l) | P r0) F r0 =
  \sum_(r0 <- (a :: l)) F r0 - \sum_(r0 <- (a :: l) | ~~ P r0) F r0

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

      rewrite !big_cons !IHl; clear IHl.

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

1 subgoal (ID 178)
  
  I : eqType
  r : seq I
  P : pred I
  F : I -> nat
  a : I
  l : seq I
  ============================
  (if P a
   then F a + (\sum_(r0 <- l) F r0 - \sum_(r0 <- l | ~~ P r0) F r0)
   else \sum_(r0 <- l) F r0 - \sum_(r0 <- l | ~~ P r0) F r0) =
  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.

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

1 subgoal (ID 181)
  
  I : eqType
  r : seq I
  P : pred I
  F : I -> nat
  a : I
  l : seq I
  ============================
  F a + (\sum_(r0 <- l) F r0 - \sum_(r0 <- l | ~~ P r0) F r0) =
  F a + \sum_(j <- l) F j - \sum_(j <- l | ~~ P j) F j

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

      rewrite addnBA; first by done.

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

1 subgoal (ID 194)
  
  I : eqType
  r : seq I
  P : pred I
  F : I -> nat
  a : I
  l : seq I
  ============================
  \sum_(r0 <- l | ~~ P r0) F r0 <= \sum_(r0 <- l) F r0

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

      rewrite big_mkcond leq_sum //.

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

1 subgoal (ID 212)
  
  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 _.

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

1 subgoal (ID 240)
  
  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).

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

No more subgoals.

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

    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 :
      ∀ (rs: seq I),
        uniq r →
        {subset r ≤ rs} →
        \sum_(i <- r) F i ≤ \sum_(i <- rs) F i.

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

1 subgoal (ID 110)
  
  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.
      intros rs UNIQ SUB; generalize dependent rs.

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

1 subgoal (ID 115)
  
  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.

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

1 subgoal (ID 132)
  
  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.

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

1 subgoal (ID 172)
  
  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.

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

1 subgoal (ID 193)
  
  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).

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

1 subgoal (ID 238)
  
  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).

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

1 subgoal (ID 255)
  
  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.

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

1 subgoal (ID 313)
  
  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.

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

1 subgoal (ID 349)
  
  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 /=.

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

1 subgoal (ID 360)
  
  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.

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

1 subgoal (ID 364)
  
  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.

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

1 subgoal (ID 370)
  
  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.

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

1 subgoal (ID 376)
  
  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.

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

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

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

1 subgoal (ID 537)
  
  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.

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

No more subgoals.

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

    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 :
      (∀ i, i \in r → P i → E1 i ≤ E2 i) →
      \sum_(i <- r | P i) E1 i ≤ \sum_(i <- r | P i) E2 i.

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

1 subgoal (ID 32)
  
  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.
      intros LE.

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

1 subgoal (ID 33)
  
  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.

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

1 subgoal (ID 60)
  
  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.

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

No more subgoals.

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

    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:
      (∀ i, i \in r → P i → E1 i == E2 i) →
      \sum_(i <- r | P i) E1 i == \sum_(i <- r | P i) E2 i.

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

1 subgoal (ID 51)
  
  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.
      move⇒ EQ.

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

1 subgoal (ID 52)
  
  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.

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

1 subgoal (ID 79)
  
  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.

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

2 subgoals (ID 109)
  
  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

subgoal 2 (ID 110) is:
 \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].

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

2 subgoals (ID 152)
  
  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

subgoal 2 (ID 192) is:
 E2 j <= E1 j

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

      all: by move:(EQ j IN H) ⇒ LEQ; ssrlia.

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

No more subgoals.

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

    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:
      (∀ i, i \in r → P1 i → P2 i) →
      \sum_(i <- r | P1 i) E i ≤ \sum_(i <- r | P2 i) E i.

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

1 subgoal (ID 68)
  
  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.
      intros LE.

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

1 subgoal (ID 69)
  
  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.

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

1 subgoal (ID 86)
  
  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.

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

1 subgoal (ID 128)
  
  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).
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 212)
  
  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)

subgoal 2 (ID 149) is:
 \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.

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

2 subgoals (ID 217)
  
  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

subgoal 2 (ID 149) is:
 \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.

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

2 subgoals (ID 298)
  
  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

subgoal 2 (ID 149) is:
 \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.

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

1 subgoal (ID 149)
  
  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.

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

2 subgoals (ID 369)
  
  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

subgoal 2 (ID 370) is:
 \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].

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

1 subgoal (ID 370)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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

    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:
      ∀ xs,
        (∀ x, x \in xs → P x → E1 x ≤ E2 x) →
        \sum_(x <- xs | P x) E1 x = \sum_(x <- xs | P x) E2 x →
        (∀ x, x \in xs → P x → E1 x = E2 x).

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

1 subgoal (ID 98)
  
  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.
      intros xs H1 H2 x IN PX.

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

1 subgoal (ID 104)
  
  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.

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

1 subgoal (ID 133)
  
  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.

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

2 subgoals (ID 165)
  
  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

subgoal 2 (ID 167) is:
 E1 x = E2 x

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

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

1 subgoal (ID 165)
  
  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 //.

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

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

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

1 subgoal (ID 269)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 283)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 167) is:
 E1 x = E2 x

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

}

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

1 subgoal (ID 167)
  
  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.

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

2 subgoals (ID 317)
  
  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 x0 : I, x0 \in xs -> P x0 -> E1 x0 <= E2 x0

subgoal 2 (ID 322) is:
 E1 x = E2 x

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

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

1 subgoal (ID 317)
  
  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 x0 : I, x0 \in xs -> P x0 -> E1 x0 <= E2 x0

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

intros x' IN' PX'.

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

1 subgoal (ID 325)
  
  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.

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

1 subgoal (ID 326)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 322) is:
 E1 x = E2 x

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

}

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

1 subgoal (ID 322)
  
  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.

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

1 subgoal (ID 410)
  
  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: ∀ a b c d, a + b = c + d → a ≤ c → b ≥ d by intros; ssrlia.

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

1 subgoal (ID 668)
  
  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].
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 749)
  
  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

subgoal 2 (ID 750) is:
 E1 x = E2 x

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

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

1 subgoal (ID 749)
  
  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.

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

1 subgoal (ID 758)
  
  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.

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

1 subgoal (ID 783)
  
  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).

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

1 subgoal (ID 785)
  
  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.

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

1 subgoal (ID 797)
  
  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.

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

1 subgoal (ID 883)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 895)
  
  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

subgoal 2 (ID 897) is:
 E1 x = E2 x

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

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

1 subgoal (ID 895)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals

subgoal 1 (ID 897) is:
 E1 x = E2 x
subgoal 2 (ID 750) is:
 E1 x = E2 x

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

}

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

1 subgoal (ID 897)
  
  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'.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 750) is:
 E1 x = E2 x

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

}

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

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

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

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

1 subgoal (ID 750)
  
  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.

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

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

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

1 subgoal (ID 1119)
  
  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_(x0 <- xs | P x0) E1 x0 = \sum_(x0 <- xs | P x0) E2 x0

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

        specialize (H1 a).

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

1 subgoal (ID 1122)
  
  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_(x0 <- xs | P x0) E1 x0 = \sum_(x0 <- xs | P x0) E2 x0

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

        feed_n 2 (H1); [ by rewrite in_cons; apply/orP; left | by done | ].

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

1 subgoal (ID 1134)
  
  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_(x0 <- xs | P x0) E1 x0 = \sum_(x0 <- xs | P x0) E2 x0

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

        move: (EqLeq
                 (E1 a) (\sum_(j <- xs | P j) E1 j)
                 (E2 a) (\sum_(j <- xs | P j) E2 j) H2 H1) ⇒ Q.

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

1 subgoal (ID 1178)
  
  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_(x0 <- xs | P x0) E1 x0 = \sum_(x0 <- xs | P x0) E2 x0

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

        by apply/eqP; rewrite eqn_leq; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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

}

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

No more subgoals.

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

    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:
        (∀ 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.

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

1 subgoal (ID 119)
  
  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.
      move⇒ LEQ.

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

1 subgoal (ID 120)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 137)
  
  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 subh2.

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

3 subgoals (ID 218)
  
  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)

subgoal 2 (ID 219) is:
 E1 a <= E2 a
subgoal 3 (ID 220) is:
 \sum_(j <- l) E1 j <= \sum_(j <- l) E2 j

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

      - apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHl.

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

3 subgoals (ID 309)
  
  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

subgoal 2 (ID 219) is:
 E1 a <= E2 a
subgoal 3 (ID 220) is:
 \sum_(j <- l) E1 j <= \sum_(j <- l) E2 j

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

        by intros; apply LEQ; rewrite in_cons; apply/orP; right.

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

2 subgoals (ID 219)
  
  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

subgoal 2 (ID 220) is:
 \sum_(j <- l) E1 j <= \sum_(j <- l) E2 j

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

      - by apply LEQ; rewrite in_cons; apply/orP; left.

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

1 subgoal (ID 220)
  
  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.

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

1 subgoal (ID 400)
  
  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 _].

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

1 subgoal (ID 474)
  
  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.

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

No more subgoals.

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

    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.

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

1 subgoal (ID 25)
  
  m, n : nat
  ============================
  \sum_(m <= i < n) 0 = 0

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

  Proof.
    by rewrite big_const_nat iter_addn mul0n addn0 //.

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

No more subgoals.

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

  Qed.

In a similar way, we prove that the sum of Δ ones is equal to Δ.
  Lemma sum_of_ones:
    ∀ t Δ,
      \sum_(t ≤ x < t + Δ) 1 = Δ.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 33)
  
  ============================
  forall t Δ : nat, \sum_(t <= x < t + Δ) 1 = Δ

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

  Proof.
    move⇒ t Δ.

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

1 subgoal (ID 35)
  
  t, Δ : nat
  ============================
  \sum_(t <= x < t + Δ) 1 = Δ

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

    rewrite big_const_nat iter_addn_0.

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

1 subgoal (ID 47)
  
  t, Δ : nat
  ============================
  1 * (t + Δ - t) = Δ

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

    by ssrlia.

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

No more subgoals.

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

  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 ↔ (∀ i, m ≤ i < n → F i = 0).

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

1 subgoal (ID 49)
  
  m, n : nat
  F : nat -> nat
  ============================
  \sum_(m <= i < n) F i = 0 <-> (forall i : nat, m <= i < n -> F i = 0)

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

  Proof.
    split.

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

2 subgoals (ID 51)
  
  m, n : nat
  F : nat -> nat
  ============================
  \sum_(m <= i < n) F i = 0 -> forall i : nat, m <= i < n -> F i = 0

subgoal 2 (ID 52) is:
 (forall i : nat, m <= i < n -> F i = 0) -> \sum_(m <= i < n) F i = 0

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

    - rewrite /index_iota ⇒ /eqP.

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

2 subgoals (ID 110)
  
  m, n : nat
  F : nat -> nat
  ============================
  \sum_(i <- iota m (n - m)) F i == 0 ->
  forall i : nat, m <= i < n -> F i = 0

subgoal 2 (ID 52) is:
 (forall i : nat, m <= i < n -> F i = 0) -> \sum_(m <= i < n) F i = 0

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

      rewrite -sum_nat_eq0_nat ⇒ /allP ZERO i.

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

2 subgoals (ID 149)
  
  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

subgoal 2 (ID 52) is:
 (forall i : nat, m <= i < n -> F i = 0) -> \sum_(m <= i < n) F i = 0

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

      rewrite -mem_index_iota /index_iota ⇒ IN.

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

2 subgoals (ID 156)
  
  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

subgoal 2 (ID 52) is:
 (forall i : nat, m <= i < n -> F i = 0) -> \sum_(m <= i < n) F i = 0

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

      by apply/eqP; apply ZERO.

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

1 subgoal (ID 52)
  
  m, n : nat
  F : nat -> nat
  ============================
  (forall i : nat, m <= i < n -> F i = 0) -> \sum_(m <= i < n) F i = 0

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

    - move⇒ ZERO.

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

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

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

1 subgoal (ID 229)
  
  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.

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

No more subgoals.

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

  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:
    ∀ f t Δ,
      \sum_(t ≤ x < t + Δ) f x < Δ →
      ∃ x, t ≤ x < t + Δ ∧ f x = 0.

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

1 subgoal (ID 62)
  
  ============================
  forall (f : nat -> nat) (t Δ : nat),
  \sum_(t <= x < t + Δ) f x < Δ -> exists x : nat, t <= x < t + Δ /\ f x = 0

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

  Proof.
    induction Δ; intros; first by rewrite ltn0 in H.

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

1 subgoal (ID 74)
  
  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.

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

2 subgoals (ID 123)
  
  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

subgoal 2 (ID 125) is:
 exists x : nat, t <= x < t + Δ.+1 /\ f x = 0

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

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

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

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

∃ (t + Δ); split; last by done.

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

1 subgoal (ID 129)
  
  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].
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 125) is:
 exists x : nat, t <= x < t + Δ.+1 /\ f x = 0

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

}

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

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

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

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

1 subgoal (ID 125)
  
  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.

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

1 subgoal (ID 283)
  
  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Δ.

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

2 subgoals (ID 284)
  
  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 < Δ

subgoal 2 (ID 289) is:
 exists x : nat, t <= x < (t + Δ).+1 /\ f x = 0

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

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

1 subgoal (ID 284)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 289) is:
 exists x : nat, t <= x < (t + Δ).+1 /\ f x = 0

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

}

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

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

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

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

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

      ∃ z; split; last by done.

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

1 subgoal (ID 364)
  
  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.

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

1 subgoal (ID 392)
  
  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.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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

}

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

No more subgoals.

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

  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:
    ∀ n F G,
      (∀ 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)).
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 84)
  
  ============================
  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.
    intros n F G ALL.

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

1 subgoal (ID 88)
  
  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.

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

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

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

1 subgoal (ID 141)
  
  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.

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

No more subgoals.

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

  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:
    ∀ (T : eqType) (r : seq T) (P : T → bool) (F : T → nat),
      reflect (∃ i, i \in r ∧ P i ∧ 0 < F i) (0 < \sum_(i <- r | P i) F i).

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

1 subgoal (ID 97)
  
  ============================
  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.
    intros; apply: (iffP idP); intros.

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

2 subgoals (ID 135)
  
  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

subgoal 2 (ID 136) is:
 0 < \sum_(i <- r | P i) F i

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

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

1 subgoal (ID 135)
  
  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.

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

1 subgoal (ID 152)
  
  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.

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

1 subgoal (ID 221)
  
  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.

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

4 subgoals (ID 248)
  
  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

subgoal 2 (ID 249) is:
 exists i : T, i \in a :: r /\ P i /\ 0 < F i
subgoal 3 (ID 259) is:
 exists i : T, i \in a :: r /\ P i /\ 0 < F i
subgoal 4 (ID 260) is:
 exists i : T, i \in a :: r /\ P i /\ 0 < F i

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

      - ∃ a; repeat split; [by rewrite in_cons; apply/orP; left | by done | by done].

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

3 subgoals (ID 249)
  
  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

subgoal 2 (ID 259) is:
 exists i : T, i \in a :: r /\ P i /\ 0 < F i
subgoal 3 (ID 260) is:
 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.

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

3 subgoals (ID 443)
  
  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

subgoal 2 (ID 259) is:
 exists i : T, i \in a :: r /\ P i /\ 0 < F i
subgoal 3 (ID 260) is:
 exists i : T, i \in a :: r /\ P i /\ 0 < F i

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

        apply IHr in H; destruct H as [i [IN [Pi POS]]].

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

3 subgoals (ID 458)
  
  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 i0 : T, i0 \in a :: r /\ P i0 /\ 0 < F i0

subgoal 2 (ID 259) is:
 exists i : T, i \in a :: r /\ P i /\ 0 < F i
subgoal 3 (ID 260) is:
 exists i : T, i \in a :: r /\ P i /\ 0 < F i

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

        by (∃ i; repeat split; [rewrite in_cons;apply/orP;right | | ]).

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

2 subgoals (ID 259)
  
  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

subgoal 2 (ID 260) is:
 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]]].

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

2 subgoals (ID 517)
  
  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 i0 : T, i0 \in a :: r /\ P i0 /\ 0 < F i0

subgoal 2 (ID 260) is:
 exists i : T, i \in a :: r /\ P i /\ 0 < F i

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

        by (∃ i; repeat split; [rewrite in_cons;apply/orP;right | | ]).

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

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

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

1 subgoal (ID 576)
  
  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 i0 : T, i0 \in a :: r /\ P i0 /\ 0 < F i0

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

        by (∃ i; repeat split; [rewrite in_cons;apply/orP;right | | ]).

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

1 subgoal

subgoal 1 (ID 136) is:
 0 < \sum_(i <- r | P i) F i

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

    }

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

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

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

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

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

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

1 subgoal (ID 652)
  
  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_(i0 <- r | P i0) F i0

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

      rewrite (big_rem i) //=; rewrite Pi.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 693)
  
  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.

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

No more subgoals.

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

    }

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

No more subgoals.

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

  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: ∀ 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.

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

1 subgoal (ID 27)
  
  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.
    induction d; first by rewrite !addn0 !big_geq.

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

1 subgoal (ID 43)
  
  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.

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

1 subgoal (ID 131)
  
  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.

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

1 subgoal (ID 508)
  
  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.

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

No more subgoals.

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

  Qed.

End SumOfTwoIntervals.