Update util files

util/all.v

 Require Export rt.util.tactics.
 Require Export rt.util.notation.
 Require Export rt.util.bigcat.
+Require Export rt.util.pick.
 Require Export rt.util.bigord.
 Require Export rt.util.counting.
 Require Export rt.util.div_mod.
@@ -16,4 +17,4 @@ Require Export rt.util.sum.
 Require Export rt.util.minmax.
 Require Export rt.util.seqset.
 Require Export rt.util.step_function.
-Require Export rt.util.pick.
\ No newline at end of file
+Require Export rt.util.epsilon.

util/list.v

@@ -109,6 +109,52 @@ Section UniqList.
   
 End UniqList.
 
+(* Additional lemmas about rem for lists. *)
+Section RemList.
+  
+  (* We prove that if x lies in xs excluding y, then x also lies in xs. *)
+  Lemma rem_in:
+    forall (T: eqType) (x y: T) (xs: seq T),
+      x \in rem y xs -> x \in xs.
+  Proof.
+    clear; intros.
+    induction xs; simpl in H.
+    { by rewrite in_nil in H. }
+    { rewrite in_cons; apply/orP.
+      destruct (a == y) eqn:EQ. 
+      { by move: EQ => /eqP EQ; subst a; right. }
+      { move: H; rewrite in_cons; move => /orP [/eqP H | H].
+        - by subst a; left.
+        - by right; apply IHxs.
+      }
+    }
+  Qed.
+
+  (* We prove that if we remove an element x for which P x from 
+     a filter, then the size of the filter decreases by 1. *)
+  Lemma filter_size_rem: 
+    forall (T: eqType) (x:T) (xs: seq T) (P: T -> bool), 
+      (x \in xs) ->
+      P x ->
+      size [seq y <- xs | P y] = size [seq y <- rem x xs | P y] + 1.
+  Proof.
+    clear; intros.
+    induction xs; first by inversion H.
+    move: H; rewrite in_cons; move => /orP [/eqP H | H]; subst.
+    { by simpl; rewrite H0 -[X in X = _]addn1 eq_refl. }
+    { specialize (IHxs H); simpl in *. 
+      case EQab: (a == x); simpl.
+      { move: EQab => /eqP EQab; subst.
+          by rewrite H0 addn1. }
+      { case Pa: (P a); simpl.
+        - by rewrite IHxs !addn1.
+        - by rewrite IHxs.
+      }
+    }
+  Qed.
+
+End RemList.
+
 (* Additional lemmas about list zip. *)
 Section Zip.
   
@@ -697,4 +743,89 @@ Section Order.
       rel x2 x1 ->
       x1 = x2.
 
-End Order.
\ No newline at end of file
+End Order.
+
+(* In this section we prove some additional lemmas about sequences. *)
+Section AdditionalLemmas.
+
+  (* We define a local function max over lists using foldl and maxn. *)
+  Let max := foldl maxn 0.
+  
+  (* We prove that max {x, xs} is equal to max {x, max xs}. *)
+  Lemma seq_max_cons: forall x xs, max (x :: xs) = maxn x (max xs).
+  Proof.
+    have L: forall s x xs, foldl maxn s (x::xs) = maxn x (foldl maxn s xs).
+    { clear; intros. 
+      generalize dependent s; generalize dependent x.
+      induction xs.
+      { by intros; rewrite maxnC. }
+      { intros; simpl in *.
+          by rewrite maxnC IHxs [maxn s a]maxnC IHxs maxnA [maxn s x]maxnC.
+      }
+    }
+      by intros; unfold max; apply L.
+  Qed.
+
+  (* We prove that for any two sequences xs and ys the fact that xs is a subsequence 
+     of ys implies that the size of xs is at most the size of ys. *)
+  Lemma subseq_leq_size:
+    forall {T: eqType} (xs ys: seq T),
+      uniq xs ->
+      (forall x, x \in xs -> x \in ys) ->
+      size xs <= size ys.
+  Proof.
+    clear; intros ? ? ? UNIQ SUB.
+    have Lem:
+      forall a ys,
+        (a \in ys) -> 
+        exists ysl ysr, ys = ysl ++ [::a] ++ ysr.
+    { clear; intros ? ? ? SUB.
+      induction ys; first by done.
+      move: SUB; rewrite in_cons; move => /orP [/eqP EQ|IN].
+      - by subst; exists [::], ys.
+      - feed IHys; first by done.
+        clear IN; move: IHys => [ysl [ysr EQ]].
+          by subst; exists(a0::ysl), ysr.
+    }
+    have EXm: exists m, size ys <= m.
+    { by exists (size ys). }
+    move: EXm => [m SIZEm].
+    move: SIZEm UNIQ SUB; move: xs ys.
+    induction m.
+    { intros.
+      move: SIZEm; rewrite leqn0 size_eq0; move => /eqP SIZEm; subst ys.
+      destruct xs; first by done.
+      specialize (SUB s).
+      feed SUB; first by rewrite in_cons; apply/orP; left.
+        by done.
+    }
+    { intros.
+      destruct xs as [ | x xs]; first by done.
+      specialize (@Lem _ x ys).
+      feed Lem.
+      { by apply SUB; rewrite in_cons; apply/orP; left. }
+      move: Lem => [ysl [ysr EQ]]; subst ys.
+      rewrite !size_cat; simpl; rewrite -addnC add1n addSn ltnS -size_cat.
+      eapply IHm.
+      - move: SIZEm; rewrite !size_cat; simpl; move => SIZE.
+          by rewrite add1n addnS ltnS addnC in SIZE.
+      - by move: UNIQ; rewrite cons_uniq; move => /andP [_ UNIQ].
+      - intros a IN.
+        destruct (a == x) eqn: EQ.
+        { exfalso.
+          move: EQ UNIQ; rewrite cons_uniq; move => /eqP EQ /andP [NIN UNIQ].
+            by subst; move: NIN => /negP NIN; apply: NIN.
+        }
+        { specialize (SUB a).
+          feed SUB.
+          { by rewrite in_cons; apply/orP; right. }
+          clear IN; move: SUB; rewrite !mem_cat; move => /orP [IN| /orP [IN|IN]].
+          - by apply/orP; right.
+          - exfalso.
+              by  move: IN; rewrite in_cons; move => /orP [IN|IN]; [rewrite IN in EQ | ].
+          - by apply/orP; left.
+        }
+    }
+  Qed.
+
+End AdditionalLemmas.
\ No newline at end of file

util/minmax.v

@@ -514,14 +514,55 @@ End MinMaxSeq.
 
 (* Additional lemmas about max. *)
 Section ExtraLemmas.
-  
-  Lemma leq_big_max I r (P : pred I) (E1 E2 : I -> nat) :
-    (forall i, P i -> E1 i <= E2 i) ->
-      \max_(i <- r | P i) E1 i <= \max_(i <- r | P i) E2 i.
+
+  Lemma leq_bigmax_cond_seq (T : eqType) (P : pred T) (r : seq T) F i0 :
+    i0 \in r -> P i0 -> F i0 <= \max_(i <- r | P i) F i.
+  Proof.
+    intros IN0 Pi0; by rewrite (big_rem i0) //= Pi0 leq_maxl.
+  Qed.
+
+  Lemma bigmax_sup_seq:
+    forall (T: eqType) (i: T) r (P: pred T) m F,
+      i \in r -> P i -> m <= F i -> m <= \max_(i <- r| P i) F i.
+  Proof.
+    intros.
+    induction r.
+    - by rewrite in_nil  in H.
+      move: H; rewrite in_cons; move => /orP [/eqP EQA | IN].
+      {
+        clear IHr; subst a.
+        rewrite (big_rem i) //=; last by rewrite in_cons; apply/orP; left.
+        apply leq_trans with (F i); first by done.
+          by rewrite H0 leq_maxl.
+      }
+      {
+        apply leq_trans with (\max_(i0 <- r | P i0) F i0); first by apply IHr.
+        rewrite [in X in _ <= X](big_rem a) //=; last by rewrite in_cons; apply/orP; left.
+
+        have Ob: a == a; first by done.
+          by rewrite Ob leq_maxr.
+      }
+  Qed.
+
+  Lemma bigmax_leq_seqP (T : eqType) (P : pred T) (r : seq T) F m :
+    reflect (forall i, i \in r -> P i -> F i <= m)
+            (\max_(i <- r | P i) F i <= m).
+  Proof.
+    apply: (iffP idP) => leFm => [i IINR Pi|];
+      first by apply: leq_trans leFm; apply leq_bigmax_cond_seq.
+    rewrite big_seq_cond; elim/big_ind: _ => // m1 m2.
+      by intros; rewrite geq_max; apply/andP; split. 
+      by move: m2 => /andP [M1IN Pm1]; apply: leFm.
+  Qed.
+
+  Lemma leq_big_max (T : eqType) (P : pred T) (r : seq T) F1 F2 :
+    (forall i, i \in r -> P i -> F1 i <= F2 i) ->
+    \max_(i <- r | P i) F1 i <= \max_(i <- r | P i) F2 i.
   Proof.
-    move => leE12; elim/big_ind2 : _ => // m1 m2 n1 n2.
-    intros LE1 LE2; rewrite leq_max; unfold maxn.
-    by destruct (m2 < n2) eqn:LT; [by apply/orP; right | by apply/orP; left].
+    intros; apply /bigmax_leq_seqP; intros.
+    specialize (H i); feed_n 2 H; try(done).
+    rewrite (big_rem i) //=; rewrite H1.
+      by apply leq_trans with (F2 i); [ | rewrite leq_maxl].
   Qed.
 
   Lemma bigmax_ord_ltn_identity n :

util/nat.v

@@ -22,7 +22,7 @@ Section NatLemmas.
       n1 >= n2 ->
       (m1 + n1) - (m2 + n2) = m1 - m2 + (n1 - n2).
   Proof. by ins; ssromega. Qed.
-
+  
   Lemma subh3 :
     forall m n p,
       m + p <= n ->
@@ -33,6 +33,21 @@ Section NatLemmas.
     by rewrite subh1 // -addnBA // subnn addn0.
   Qed.
 
+  (* subh3: forall m n p : nat, m + p <= n -> p <= n -> m <= n - p *)
+  (*                 unnecessary condition -- ^^^^^^^^^ *)
+  (* TODO: del subh3 *)
+  Lemma subh3_ext:
+    forall m n p,
+      m + p <= n ->
+      m <= n - p.
+  Proof.
+    clear.
+    intros.
+    apply subh3; first by done.
+    apply leq_trans with (m+p); last by done.
+      by rewrite leq_addl.
+  Qed.
+
   Lemma subh4:
     forall m n p,
       m <= n ->

util/step_function.v

@@ -85,5 +85,50 @@ Section StepFunction.
     End ExistsIntermediateValue.
 
   End Lemmas.
+  
+  (* In this section, we prove an analogue of the intermediate
+     value theorem, but for predicates of natural numbers. *) 
+  Section ExistsIntermediateValuePredicates. 
+
+    (* Let P be any predicate on natural numbers. *)
+    Variable P: nat -> bool.
+
+    (* Consider a time interval [t1,t2] such that ... *)
+    Variables t1 t2: nat.
+    Hypothesis H_t1_le_t2: t1 <= t2.
+
+    (* ... P doesn't hold for t1 ... *)
+    Hypothesis H_not_P_at_t1: ~~ P t1.
+
+    (* ... but holds for t2. *)
+    Hypothesis H_P_at_t2: P t2.
+    
+    (* Then we prove that within time interval [t1,t2] there exists time 
+       instant t such that t is the first time instant when P holds. *)
+    Lemma exists_first_intermediate_point:
+      exists t, (t1 < t <= t2) /\ (forall x, t1 <= x < t -> ~~ P x) /\ P t.
+    Proof.
+      have EX: exists x, P x && (t1 < x <= t2).
+      { exists t2.
+        apply/andP; split; first by done.
+        apply/andP; split; last by done.
+        move: H_t1_le_t2; rewrite leq_eqVlt; move => /orP [/eqP EQ | NEQ1]; last by done.
+          by exfalso; subst t2; move: H_not_P_at_t1 => /negP NPt1. 
+      }
+      have MIN := ex_minnP EX.
+      move: MIN => [x /andP [Px /andP [LT1 LT2]] MIN]; clear EX.
+      exists x; repeat split; [ apply/andP; split | | ]; try done.
+      move => y /andP [NEQ1 NEQ2]; apply/negPn; intros Py.
+      feed (MIN y). 
+      { apply/andP; split; first by done.
+        apply/andP; split.
+        - move: NEQ1. rewrite leq_eqVlt; move => /orP [/eqP EQ | NEQ1]; last by done.
+            by exfalso; subst y; move: H_not_P_at_t1 => /negP NPt1. 
+        - by apply ltnW, leq_trans with x.
+      }
+        by move: NEQ2; rewrite ltnNge; move => /negP NEQ2.
+    Qed.
+    
+  End ExistsIntermediateValuePredicates.  
 
 End StepFunction.
\ No newline at end of file

util/sum.v

 Require Import rt.util.tactics rt.util.notation rt.util.sorting rt.util.nat.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
 
-(* Lemmas about arithmetic with sums. *)
-Section SumArithmetic.
-
-  (* Inequality with sums is monotonic with their functions. *)
-  Lemma sum_diff_monotonic :
-    forall n G F,
-      (forall i : nat, i < n -> G i <= F i) ->
-      (\sum_(0 <= i < n) (G i)) <= (\sum_(0 <= i < n) (F i)).
-  Proof.
-    intros n G F ALL.
-    rewrite big_nat_cond [\sum_(0 <= i < n) F i]big_nat_cond.
-    apply leq_sum; intros i LT; rewrite andbT in LT.
-    move: LT => /andP LT; des.
-    by apply ALL, leq_trans with (n := n); ins.
-  Qed.
-
-  Lemma sum_diff :
-    forall n F G,
-      (forall i (LT: 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)).       
-  Proof.
-    intros n F G ALL.
-    induction n; ins; first by rewrite 3?big_geq.
-    assert (ALL': forall i, i < n -> G i <= F i).
-      by ins; apply ALL, leq_trans with (n := n); ins.
-    rewrite 3?big_nat_recr // IHn //; simpl.
-    rewrite subh1; last by apply sum_diff_monotonic.
-    rewrite subh2 //; try apply sum_diff_monotonic; ins.
-    rewrite subh1; ins; apply sum_diff_monotonic; ins.
-    by apply ALL; rewrite ltnS leqnn. 
-  Qed.
-
-  Lemma telescoping_sum :
-    forall (T: Type) (F: T->nat) r (x0: T),
-    (forall i, i < (size r).-1 -> F (nth x0 r i) <= F (nth x0 r i.+1)) ->
-      F (nth x0 r (size r).-1) - F (nth x0 r 0) =
-        \sum_(0 <= i < (size r).-1) (F (nth x0 r (i.+1)) - F (nth x0 r i)).
-  Proof.
-    intros T F r x0 ALL.
-    have ADD1 := big_add1.
-    have RECL := big_nat_recl.
-    specialize (ADD1 nat 0 addn 0 (size r) (fun x => true) (fun i => F (nth x0 r i))).
-    specialize (RECL nat 0 addn (size r).-1 0 (fun i => F (nth x0 r i))).
-    rewrite sum_diff; last by ins.
-    rewrite addmovr; last by rewrite -[_.-1]add0n; apply prev_le_next; try rewrite add0n leqnn.
-    rewrite subh1; last by apply sum_diff_monotonic.
-    rewrite addnC -RECL //.
-    rewrite addmovl; last by rewrite big_nat_recr // -{1}[\sum_(_ <= _ < _) _]addn0; apply leq_add.
-    by rewrite addnC -big_nat_recr.
-  Qed.
-
-  Lemma leq_sum_sub_uniq :
-    forall (T: eqType) (r1 r2: seq T) F,
-      uniq r1 ->
-      {subset r1 <= r2} ->
-      \sum_(i <- r1) F i <= \sum_(i <- r2) F i.
-  Proof.
-    intros T r1 r2 F UNIQ SUB; generalize dependent r2.
-    induction r1 as [| x r1' IH]; first by ins; rewrite big_nil.
-    {
-      intros r2 SUB.
-      assert (IN: x \in r2).
-        by apply SUB; rewrite in_cons eq_refl orTb.
-      simpl in UNIQ; move: UNIQ => /andP [NOTIN UNIQ]; specialize (IH UNIQ).
-      destruct (splitPr IN).
-      rewrite big_cat 2!big_cons /= addnA [_ + F x]addnC -addnA leq_add2l.
-      rewrite mem_cat in_cons eq_refl in IN.
-      rewrite -big_cat /=.
-      apply IH; red; intros x0 IN0.
-      rewrite mem_cat.
-      feed (SUB x0); first by rewrite in_cons IN0 orbT.
-      rewrite mem_cat in_cons in SUB.
-      move: SUB => /orP [SUB1 | /orP [/eqP EQx | SUB2]];
-        [by rewrite SUB1 | | by rewrite SUB2 orbT].
-      by rewrite -EQx IN0 in NOTIN.
-    }
-  Qed.
-    
-End SumArithmetic.
-
-(* Additional lemmas about sum. *)
+(* Lemmas about sum. *)
 Section ExtraLemmas.
   
   Lemma extend_sum :
@@ -97,7 +16,7 @@ Section ExtraLemmas.
     rewrite -> big_cat_nat with (m := t1') (n := t1); try (by done); simpl;
       last by apply leq_trans with (n := t2).
     rewrite -> big_cat_nat with (p := t2') (n := t2); try (by done); simpl.
-    by rewrite addnC -addnA; apply leq_addr.
+      by rewrite addnC -addnA; apply leq_addr.
   Qed.
 
   Lemma leq_sum_nat m n (P : pred nat) (E1 E2 : nat -> nat) :
@@ -106,7 +25,7 @@ Section ExtraLemmas.
   Proof.
     intros LE.
     rewrite big_nat_cond [\sum_(_ <= _ < _| P _)_]big_nat_cond.
-    by apply leq_sum; move => j /andP [IN H]; apply LE.
+      by apply leq_sum; move => j /andP [IN H]; apply LE.
   Qed.
 
   Lemma leq_sum_seq (I: eqType) (r: seq I) (P : pred I) (E1 E2 : I -> nat) :
@@ -115,7 +34,7 @@ Section ExtraLemmas.
   Proof.
     intros LE.
     rewrite big_seq_cond [\sum_(_ <- _| P _)_]big_seq_cond.
-    by apply leq_sum; move => j /andP [IN H]; apply LE.
+      by apply leq_sum; move => j /andP [IN H]; apply LE.
   Qed.
 
   Lemma sum_nat_eq0_nat (T : eqType) (F : T -> nat) (r: seq T) :
@@ -128,7 +47,7 @@ Section ExtraLemmas.
         first by rewrite big_const_seq iter_addn mul0n addn0 leqnn.
       intro i; rewrite andbT; intros IN.
       specialize (ZERO i); rewrite IN in ZERO.
-      by move: ZERO => /implyP ZERO; apply/eqP; apply ZERO.
+        by move: ZERO => /implyP ZERO; apply/eqP; apply ZERO.
     }
     {
       apply negbT in ZERO; rewrite -has_predC in ZERO.
@@ -136,7 +55,7 @@ Section ExtraLemmas.
       rewrite (big_rem x) /=; last by done.
       symmetry; apply negbTE; rewrite neq_ltn; apply/orP; right.
       apply leq_trans with (n := F x); last by apply leq_addr.
-      by rewrite lt0n.
+        by rewrite lt0n.
     }
   Qed.
   
@@ -153,7 +72,7 @@ Section ExtraLemmas.
       case TRUE: (P i); last by done.
       move: (REDUCE i (conj LE TRUE)) => [LE' TRUE'].
       rewrite (big_rem i); last by rewrite mem_index_iota.
-      by rewrite TRUE' eq_refl.
+        by rewrite TRUE' eq_refl.
     }
     {
       apply leq_sum_nat; intros i LE TRUE.
@@ -162,12 +81,242 @@ Section ExtraLemmas.
       {
         rewrite big_nat_cond big1; first by done.
         move => i' /andP [LE'' _]; case EQ: (_ == _); last by done.
-        by move: EQ => /eqP EQ; subst; rewrite LE'' in LE'.
+          by move: EQ => /eqP EQ; subst; rewrite LE'' in LE'.
       }
       rewrite (bigD1_seq i) /=; [ | by rewrite mem_index_iota | by rewrite iota_uniq ].
       rewrite eq_refl big1; first by done.
-      by move => i' /negbTE NEQ; rewrite NEQ.
+        by move => i' /negbTE NEQ; rewrite NEQ.
+    }
+  Qed.
+
+  Lemma sum_seq_gt0P:
+    forall (T:eqType) (r: seq T) (F: T -> nat),
+      reflect (exists i, i \in r /\ 0 < F i) (0 < \sum_(i <- r) F i).
+  Proof.
+    intros; apply: (iffP idP); intros.
+    {
+      induction r; first by rewrite big_nil in H.
+      destruct (F a > 0) eqn:POS.
+      exists a; split; [by rewrite in_cons; apply/orP; left | by done].
+      apply negbT in POS; rewrite -leqNgt leqn0 in POS; move: POS => /eqP POS.
+      rewrite big_cons POS add0n in H. clear POS.
+      feed IHr; first by done. move: IHr => [i [IN POS]].
+      exists i; split; [by rewrite in_cons; apply/orP;right | by done].
+    }
+    {
+      move: H => [i [IN POS]].
+      rewrite (big_rem i) //=.
+      apply leq_trans with (F i); [by done | by rewrite leq_addr].
+    }
+  Qed.
+
+  Lemma leq_pred_sum:
+    forall (T:eqType) (r: seq T) (P1 P2: pred T) F, 
+      (forall i, P1 i -> P2 i) ->
+      \sum_(i <- r | P1 i) F i <=
+      \sum_(i <- r | P2 i) F i.
+  Proof.
+    intros.
+    rewrite big_mkcond [in X in _ <= X]big_mkcond//= leq_sum //.
+    intros i _. 
+    destruct P1 eqn:P1a; destruct P2 eqn:P2a; [by done | | by done | by done].
+    exfalso.
+    move: P1a P2a => /eqP P1a /eqP P2a.
+    rewrite eqb_id in P1a; rewrite eqbF_neg in P2a.
+    move: P2a => /negP P2a.
+      by apply P2a; apply H.
+  Qed.
+
+  Lemma sum_notin_rem_eqn:
+    forall (T:eqType) (a: T) xs P F,
+      a \notin xs ->
+      \sum_(x <- xs | P x && (x != a)) F x = \sum_(x <- xs | P x) F x.
+  Proof.
+    intros ? ? ? ? ? NOTIN.
+    induction xs; first by rewrite !big_nil.
+    rewrite !big_cons.
+    rewrite IHxs; clear IHxs; last first.
+    { apply/memPn; intros y IN.
+      move: NOTIN => /memPn NOTIN.
+        by apply NOTIN; rewrite in_cons; apply/orP; right.
     }
+    move: NOTIN => /memPn NOTIN. 
+    move: (NOTIN a0) => NEQ.
+    feed NEQ; first by (rewrite in_cons; apply/orP; left).
+      by rewrite NEQ Bool.andb_true_r.
   Qed.
 
-End ExtraLemmas.
\ No newline at end of file
+  (* We prove that if any element of a set r is bounded by constant const, 
+     then the sum of the whole set is bounded by [const * size r]. *)
+  Lemma sum_majorant_constant:
+    forall (T: eqType) (r: seq T) (P: pred T) F const,
+      (forall a,  a \in r -> P a -> F a <= const) -> 
+      \sum_(j <- r | P j) F j <= const * (size [seq j <- r | P j]).
+  Proof.
+    clear; intros.
+    induction r; first by rewrite big_nil.
+    feed IHr.
+    { intros; apply H.
+      - by rewrite in_cons; apply/orP; right.
+      - by done. } 
+    rewrite big_cons.
+    destruct (P a) eqn:EQ.
+    { rewrite -cat1s filter_cat size_cat.
+      rewrite mulnDr.
+      apply leq_add; last by done.
+      rewrite size_filter.
+      simpl; rewrite addn0.
+      rewrite EQ muln1.
+      apply H; last by done. 
+        by rewrite in_cons; apply/orP; left. 
+    }
+    { apply leq_trans with (const * size [seq j <- r | P j]); first by done.
+      rewrite leq_mul2l; apply/orP; right.
+      rewrite -cat1s filter_cat size_cat.
+        by rewrite leq_addl.
+    }
+  Qed.
+
+  (* We prove that if for any element x of a set xs the following two statements hold 
+     (1) [F1 x] is less than or equal to [F2 x] and (2) the sum [F1 x_1, ..., F1 x_n] 
+     is equal to the sum of [F2 x_1, ..., F2 x_n], then [F1 x] is equal to [F2 x] for 
+     any element x of xs. *)
+  Lemma sum_majorant_eqn:
+    forall (T: eqType) xs F1 F2 (P: pred T),
+      (forall x, x \in xs -> P x -> F1 x <= F2 x) -> 
+      \sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
+      (forall x, x \in xs -> P x -> F1 x = F2 x).
+  Proof.
+    clear.      
+    intros T xs F1 F2 P H1 H2 x IN PX.
+    induction xs; first by done.
+    have Fact: \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j.
+    { rewrite [in X in X <= _]big_seq_cond [in X in _ <= X]big_seq_cond leq_sum //.
+      move => y /andP [INy PY].
+      apply: H1; last by done. 
+        by rewrite in_cons; apply/orP; right. }
+    feed IHxs.
+    { intros x' IN' PX'.
+      apply H1; last by done.
+        by rewrite in_cons; apply/orP; right. }
+    rewrite big_cons [RHS]big_cons in H2.
+    have EqLeq: forall a b c d, a + b = c + d -> a <= c -> b >= d.
+    { clear; intros.
+      rewrite leqNgt; apply/negP; intros H1.
+      move: H => /eqP; rewrite eqn_leq; move => /andP [LE GE].
+      move: GE; rewrite leqNgt; move => /negP GE; apply: GE.
+        by apply leq_trans with (a + d); [rewrite ltn_add2l | rewrite leq_add2r]. }
+    move: IN; rewrite in_cons; move => /orP [/eqP EQ | IN]. 
+    { subst a.
+      rewrite PX in H2.
+      specialize (H1 x).
+      feed_n 2 H1; [ by rewrite in_cons; apply/orP; left | by done | ].
+      move: (EqLeq
+               (F1 x) (\sum_(j <- xs | P j) F1 j)
+               (F2 x) (\sum_(j <- xs | P j) F2 j) H2 H1) => Q.
+      have EQ: \sum_(j <- xs | P j) F1 j = \sum_(j <- xs | P j) F2 j. 
+      { by apply/eqP; rewrite eqn_leq; apply/andP; split. }
+        by move: H2 => /eqP; rewrite EQ eqn_add2r; move => /eqP EQ'.
+    }
+    { destruct (P a) eqn:PA; last by apply IHxs.
+      apply: IHxs; last by done.
+      specialize (H1 a).
+      feed_n 2 (H1); [ by rewrite in_cons; apply/orP; left | by done | ].
+      move: (EqLeq
+               (F1 a) (\sum_(j <- xs | P j) F1 j)
+               (F2 a) (\sum_(j <- xs | P j) F2 j) H2 H1) => Q.
+        by apply/eqP; rewrite eqn_leq; apply/andP; split.
+    }
+  Qed.
+
+  (* We prove that the sum of Δ ones is equal to Δ. *)
+  Lemma sum_of_ones:
+    forall t Δ,
+      \sum_(t <= x < t + Δ) 1 = Δ. 
+  Proof.
+    intros.
+    simpl_sum_const.
+    rewrite addnC -addnBA; last by done.
+      by rewrite subnn addn0.  
+  Qed.
+  
+End ExtraLemmas.
+
+(* Lemmas about arithmetic with sums. *)
+Section SumArithmetic.
+
+  Lemma sum_seq_diff:
+    forall (T:eqType) (r: seq T) (F G : T -> nat),
+      (forall i : T, i \in r -> G i <= F i) ->
+      \sum_(i <- r) (F i - G i) = \sum_(i <- r) F i - \sum_(i <- r) G i.
+  Proof.
+    intros.
+    induction r; first by rewrite !big_nil subn0. 
+    rewrite !big_cons subh2.
+    - apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHr.
+        by intros; apply H; rewrite in_cons; apply/orP; right.
+    - by apply H; rewrite in_cons; apply/orP; left.
+    - rewrite big_seq_cond [in X in _ <= X]big_seq_cond.
+      rewrite leq_sum //; move => i /andP [IN _].
+        by apply H; rewrite in_cons; apply/orP; right.
+  Qed.
+  
+  Lemma sum_diff:
+    forall n F G,
+      (forall i (LT: 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)).       
+  Proof.
+    intros n F G ALL.
+    rewrite sum_seq_diff; first by done.
+    move => i; rewrite mem_index_iota; move => /andP [_ LT].
+      by apply ALL.
+  Qed.
+  
+  Lemma telescoping_sum :
+    forall (T: Type) (F: T->nat) r (x0: T),
+      (forall i, i < (size r).-1 -> F (nth x0 r i) <= F (nth x0 r i.+1)) ->
+      F (nth x0 r (size r).-1) - F (nth x0 r 0) =
+      \sum_(0 <= i < (size r).-1) (F (nth x0 r (i.+1)) - F (nth x0 r i)).
+  Proof.
+    intros T F r x0 ALL.
+    have ADD1 := big_add1.
+    have RECL := big_nat_recl.
+    specialize (ADD1 nat 0 addn 0 (size r) (fun x => true) (fun i => F (nth x0 r i))).
+    specialize (RECL nat 0 addn (size r).-1 0 (fun i => F (nth x0 r i))).
+    rewrite sum_diff; last by ins.
+    rewrite addmovr; last by rewrite -[_.-1]add0n; apply prev_le_next; try rewrite add0n leqnn.
+    rewrite subh1; last by apply leq_sum_nat; move => i /andP [_ LT] _; apply ALL.
+    rewrite addnC -RECL //.
+    rewrite addmovl; last by rewrite big_nat_recr // -{1}[\sum_(_ <= _ < _) _]addn0; apply leq_add.
+      by rewrite addnC -big_nat_recr.
+  Qed.
+
+  Lemma leq_sum_sub_uniq :
+    forall (T: eqType) (r1 r2: seq T) F,
+      uniq r1 ->
+      {subset r1 <= r2} ->
+      \sum_(i <- r1) F i <= \sum_(i <- r2) F i.
+  Proof.
+    intros T r1 r2 F UNIQ SUB; generalize dependent r2.
+    induction r1 as [| x r1' IH]; first by ins; rewrite big_nil.
+    {
+      intros r2 SUB.
+      assert (IN: x \in r2).
+        by apply SUB; rewrite in_cons eq_refl orTb.
+        simpl in UNIQ; move: UNIQ => /andP [NOTIN UNIQ]; specialize (IH UNIQ).
+        destruct (splitPr IN).
+        rewrite big_cat 2!big_cons /= addnA [_ + F x]addnC -addnA leq_add2l.
+        rewrite mem_cat in_cons eq_refl in IN.
+        rewrite -big_cat /=.
+        apply IH; red; intros x0 IN0.
+        rewrite mem_cat.
+        feed (SUB x0); first by rewrite in_cons IN0 orbT.
+        rewrite mem_cat in_cons in SUB.
+        move: SUB => /orP [SUB1 | /orP [/eqP EQx | SUB2]];
+                       [by rewrite SUB1 | | by rewrite SUB2 orbT].
+          by rewrite -EQx IN0 in NOTIN.
+    }
+  Qed.
+  
+End SumArithmetic.
\ No newline at end of file