various cleanups and simplifications in util

Pierre's cleanups from !190, minus the TODO annotations.

CC: @proux

util/sum.v

@@ -149,6 +149,9 @@ Section SumsOverSequences.
 
 End SumsOverSequences.
 
+(** We continue establishing properties of sums over sequences, but start a new
+    section here because some of the below proofs depend lemmas in the preceding
+    section in their full generality. *)
 Section SumsOverSequences.
 
   (** Consider any type [I] with a decidable equality ... *)
@@ -160,49 +163,48 @@ Section SumsOverSequences.
   (** ... and a predicate [P]. *)
   Variable (P : pred I).
 
-  Section SumOfTwoFunctions.
-
-    (** Consider three functions that yield natural numbers. *)
-    Variable (E E1 E2 : I -> nat).
-
-    (** Besides earlier introduced predicate [P], we add two additional predicates [P1] and [P2]. *)
-    Variable (P1 P2 : pred I).
-
-    Lemma ltn_sum_leq_seq j : j \in r -> P j -> E1 j < E2 j ->
-      (forall i, i \in r -> P i -> E1 i <= E2 i) ->
-      \sum_(x <- r | P x) E1 x < \sum_(x <- r | P x) E2 x.
-    Proof.
-      move=> jr Pj ltj le.
-      rewrite (big_rem j)// [X in _ < X](big_rem j)//= Pj -addSn leq_add//.
-      apply: leq_sum_seq => i /mem_rem; exact: le.
-    Qed.
+  (** Consider two functions that yield natural numbers. *)
+  Variable (E1 E2 : I -> nat).
+
+  (** First, as an auxiliary lemma, we observe that, if [E1 j] is less than [E2
+      j] for some element [j] involved in a summation (filtered by [P]), then
+      the corresponding totals are not equal. *)
+  Lemma ltn_sum_leq_seq j :
+    j \in r ->
+    P j ->
+    E1 j < E2 j ->
+    (forall i, i \in r -> P i -> E1 i <= E2 i) ->
+    \sum_(x <- r | P x) E1 x < \sum_(x <- r | P x) E2 x.
+  Proof.
+    move=> jr Pj ltj le.
+    rewrite (big_rem j)// [X in _ < X](big_rem j)//= Pj -addSn leq_add//.
+    apply: leq_sum_seq => i /mem_rem; exact: le.
+  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 eq_sum_leq_seq :
-      (forall i, i \in r -> P i -> E1 i <= E2 i) ->
-      \sum_(x <- r | P x) E1 x == \sum_(x <- r | P x) E2 x
+  (** Next, we prove that if for any element i of a set [r] the following two
+      statements hold (1) [E1 i] is less than or equal to [E2 i] and (2) the sum
+      [E1 x_1, ..., E1 x_n] is equal to the sum of [E2 x_1, ..., E2 x_n], then
+      [E1 x] is equal to [E2 x] for any element x of [xs]. *)
+  Lemma eq_sum_leq_seq :
+    (forall i, i \in r -> P i -> E1 i <= E2 i) ->
+    \sum_(x <- r | P x) E1 x == \sum_(x <- r | P x) E2 x
       = all (fun x => E1 x == E2 x) [seq x <- r | P x].
-    Proof.
-      move=> le; rewrite all_filter; case aE: all.
-        apply: eq_sum_seq => i ir Pi; move: aE => /allP/(_ i ir)/implyP; exact.
-      have [j /andP[jr Pj] ltj] : exists2 j, (j \in r) && P j & E1 j < E2 j.
-        have /negbT := aE; rewrite -has_predC => /hasP[j jr /=].
-        rewrite negb_imply => /andP[Pj neq].
-        by exists j; first exact/andP; rewrite ltn_neqAle neq le.
-      by apply/negbTE; rewrite neq_ltn (ltn_sum_leq_seq j).
-    Qed.
-
-  End SumOfTwoFunctions.
+  Proof.
+    move=> le; rewrite all_filter; case aE: all.
+    apply: eq_sum_seq => i ir Pi; move: aE => /allP/(_ i ir)/implyP; exact.
+    have [j /andP[jr Pj] ltj] : exists2 j, (j \in r) && P j & E1 j < E2 j.
+    have /negbT := aE; rewrite -has_predC => /hasP[j jr /=].
+    rewrite negb_imply => /andP[Pj neq].
+    - by exists j; first exact/andP; rewrite ltn_neqAle neq le.
+    - by apply/negbTE; rewrite neq_ltn (ltn_sum_leq_seq j).
+  Qed.
 
 End SumsOverSequences.
 
 (** In this section, we prove a variety of properties of sums performed over ranges. *)
 Section SumsOverRanges.
 
-  (** In a similar way, we prove that the sum of Δ ones is equal to Δ. *)
+  (** First, we prove that the sum of Δ ones is equal to Δ. *)
   Lemma sum_of_ones:
     forall t Δ,
       \sum_(t <= x < t + Δ) 1 = Δ.