various cleanups and simplifications in util

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

CC: @proux

analysis/facts/model/workload.v

@@ -89,7 +89,7 @@ Section WorkloadFacts.
       clear H_jobs_uniq H_j_in_jobs H_t1_le_t2.
       rewrite /workload_of_jobs big_seq_cond.
       rewrite -[in X in X <= _]big_filter -[in X in _ <= X]big_filter.
-      apply leq_sum_sub_uniq; first by apply filter_uniq, arrivals_uniq.
+      apply: leq_sum_sub_uniq => //; first by apply filter_uniq, arrivals_uniq.
       move => j'; rewrite mem_filter => [/andP [/andP [A /andP [C D]] _]].
       rewrite mem_filter; apply/andP; split; first by done.
       apply job_in_arrivals_between; eauto.