Library prosa.util.sum


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

Welcome to Coq 8.11.2 (June 2020)

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

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 29)
  
  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 44)
  
  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 45) is:
 false = (\sum_(i <- r) F i == 0)

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

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

1 subgoal (ID 44)
  
  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 84)
  
  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 113)
  
  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 134)
  
  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 152)
  
  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 (ID 45)

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

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

}

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

1 subgoal (ID 45)
  
  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 45)
  
  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 280)
  
  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 328)
  
  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 345)
  
  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 401)
  
  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 402)
  
  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 42)
  
  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 76)
  
  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 77) is:
 0 < \sum_(i <- r) F i

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

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

1 subgoal (ID 76)
  
  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 94)
  
  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 151)
  
  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 152) is:
 exists i : I, i \in a :: l /\ 0 < F i

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

        - ∃ a.

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

2 subgoals (ID 154)
  
  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 152) is:
 exists i : I, i \in a :: l /\ 0 < F i

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

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

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

1 subgoal (ID 152)
  
  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 272)
  
  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 305)
  
  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 327)
  
  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 (ID 77)

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

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

}

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

1 subgoal (ID 77)
  
  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 77)
  
  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 409)
  
  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 426)
  
  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 62)
  
  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 64)
  
  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 81)
  
  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 134)
  
  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 135) is:
 a \notin l

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

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

1 subgoal (ID 134)
  
  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 171)
  
  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 173)
  
  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 179)
  
  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 (ID 135)

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

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

}

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

1 subgoal (ID 135)
  
  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 135)
  
  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 247)
  
  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 283)
  
  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 78)
  
  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 80)
  
  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 97)
  
  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 106)
  
  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 111) is:
 \sum_(j <- (a :: l) | P j) F j <= c * size [seq j <- a :: l | P j]

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

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

1 subgoal (ID 106)
  
  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 115)
  
  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 116) is:
 P a0

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

        - by rewrite in_cons; apply/orP; right.

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

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

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

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

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

1 subgoal (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 : \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 158)
  
  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 170)
  
  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 171) is:
 \sum_(j <- l | P j) F j <= c * size [seq j <- a :: l | P j]

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

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

1 subgoal (ID 170)
  
  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 195)
  
  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 196)
  
  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 239)
  
  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 240)
  
  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 (ID 171)

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

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

}

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

1 subgoal (ID 171)
  
  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 171)
  
  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 278)
  
  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 309)
  
  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 96)
  
  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 107)
  
  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 183)
  
  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 187)
  
  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 201)
  
  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 219)
  
  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 248)
  
  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 115)
  
  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 120)
  
  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 137)
  
  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 178)
  
  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 199)
  
  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 245)
  
  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 262)
  
  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 320)
  
  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 356)
  
  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 367)
  
  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 372)
  
  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 378)
  
  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 384)
  
  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 429)
  
  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 548)
  
  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 two functions that yield natural numbers.
    Variable (E1 E2 : I → nat).

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 34)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  ============================
  (forall i : I, i \in r -> P i -> E1 i <= E2 i) ->
  \sum_(i <- r | P i) E1 i <= \sum_(i <- r | P i) E2 i

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

    Proof.
      intros LE.

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

1 subgoal (ID 35)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  LE : forall i : I, i \in r -> P i -> E1 i <= E2 i
  ============================
  \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 62)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  LE : forall i : I, i \in r -> P i -> E1 i <= E2 i
  ============================
  \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 53)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  ============================
  (forall i : I, i \in r -> P i -> E1 i == E2 i) ->
  \sum_(i <- r | P i) E1 i == \sum_(i <- r | P i) E2 i

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

    Proof.
      move⇒ EQ.

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

1 subgoal (ID 54)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 81)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 111)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 112) 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 155)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 196) is:
 E2 j <= E1 j

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

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

(* ----------------------------------[ 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 85)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  ============================
  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 91)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 120)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 153)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 155) is:
 E1 x = E2 x

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

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

1 subgoal (ID 153)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 192)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 259)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 273)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 (ID 155)

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

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

}

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

1 subgoal (ID 155)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 307)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 312) is:
 E1 x = E2 x

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

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

1 subgoal (ID 307)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 315)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 316)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 (ID 312)

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

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

}

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

1 subgoal (ID 312)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 398)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 694)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 777)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 778) is:
 E1 x = E2 x

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

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

1 subgoal (ID 777)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 786)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 808)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 810)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 822)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 910)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 923)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 925) is:
 E1 x = E2 x

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

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

1 subgoal (ID 923)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 (ID 925)

subgoal 1 (ID 925) is:
 E1 x = E2 x
subgoal 2 (ID 778) is:
 E1 x = E2 x

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

}

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

1 subgoal (ID 925)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 (ID 778)

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

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

}

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

1 subgoal (ID 778)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 778)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 1133)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 1149)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 1152)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 1164)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 1208)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 107)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  ============================
  (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 108)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 125)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 206)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 207) is:
 E1 a <= E2 a
subgoal 3 (ID 208) is:
 \sum_(j <- l) E1 j <= \sum_(j <- l) E2 j

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

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

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

3 subgoals (ID 297)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 207) is:
 E1 a <= E2 a
subgoal 3 (ID 208) 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 207)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 208) is:
 \sum_(j <- l) E1 j <= \sum_(j <- l) E2 j

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

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

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

1 subgoal (ID 208)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 388)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 464)
  
  I : eqType
  r : seq I
  P : pred I
  E1, E2 : I -> nat
  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 28)
  
  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 37)
  
  ============================
  forall t Δ : nat, \sum_(t <= x < t + Δ) 1 = Δ

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

  Proof.
    move⇒ t Δ.

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

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

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

    rewrite big_const_nat iter_addn_0.

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

1 subgoal (ID 51)
  
  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 55)
  
  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 57)
  
  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 58) 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 117)
  
  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 58) 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 157)
  
  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 58) 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 164)
  
  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 58) 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 58)
  
  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 221)
  
  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 238)
  
  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 69)
  
  ============================
  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 81)
  
  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 131)
  
  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 133) is:
 exists x : nat, t <= x < t + Δ.+1 /\ f x = 0

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

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

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

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

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

}

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

1 subgoal (ID 133)
  
  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 133)
  
  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 294)
  
  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 295)
  
  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 300) is:
 exists x : nat, t <= x < (t + Δ).+1 /\ f x = 0

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

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

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

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

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

}

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

1 subgoal (ID 300)
  
  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 372)
  
  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 376)
  
  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 404)
  
  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 92)
  
  ============================
  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 96)
  
  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 104)
  
  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 150)
  
  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.

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 31)
  
  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 47)
  
  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 135)
  
  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 596)
  
  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.