Shorten a needlessly-long proof

model/schedule/uni/service.v

@@ -310,9 +310,9 @@ Module Service.
       } 
     Qed.
     
-    (* Last, we prove that overall service of jobs at each time instant is at most 1. *)
+    (* We prove that the overall service of jobs at each time instant is at most 1. *)
     Lemma service_of_jobs_le_1:
-      forall t1 t2 t P,
+      forall (t1 t2 t: time) (P: Job -> bool),
         \sum_(j <- arrivals_between t1 t2 | P j) service_at sched j t <= 1.
     Proof.
       intros t1 t2 t P.
@@ -348,6 +348,23 @@ Module Service.
           by rewrite /service_at /scheduled_at SCHED.
       }
     Qed.
+
+    (* We prove that the overall service of jobs within 
+       some time interval [t, t + Δ) is at most Δ. *)
+    Lemma total_service_of_jobs_le_delta:  
+      forall (t Δ: time) (P: Job -> bool),
+        \sum_(j <- arrivals_between t (t + Δ) | P j)
+         service_during sched j t (t + Δ) <= Δ.
+    Proof.
+      intros.
+      have EQ: \sum_(t <= x < t + Δ) 1 = Δ.
+      { by rewrite big_const_nat iter_addn mul1n addn0 -{2}[t]addn0 subnDl subn0. } 
+      rewrite -{3}EQ; clear EQ.
+      rewrite exchange_big //=.
+      rewrite leq_sum //.
+      move => t' _.
+        by apply service_of_jobs_le_1.
+    Qed.
     
     (* In this section, we introduce a connection between the cumulative 
        service, cumulative workload, and completion of jobs. *)

util/sum.v

@@ -246,14 +246,14 @@ End ExtraLemmas.
 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.
+    forall (T:eqType) (rs: seq T) (F G : T -> nat),
+      (forall i : T, i \in rs -> G i <= F i) ->
+      \sum_(i <- rs) (F i - G i) = \sum_(i <- rs) F i - \sum_(i <- rs) G i.
   Proof.
     intros.
-    induction r; first by rewrite !big_nil subn0. 
+    induction rs; first by rewrite !big_nil subn0. 
     rewrite !big_cons subh2.
-    - apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHr.
+    - apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHrs.
         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.
@@ -272,6 +272,21 @@ Section SumArithmetic.
     move => i; rewrite mem_index_iota; move => /andP [_ LT].
       by apply ALL.
   Qed.
+
+  Lemma sum_pred_diff:
+    forall (T: eqType) (rs: seq T) (P: T -> bool) (F: T -> nat),
+      \sum_(r <- rs | P r) F r =
+      \sum_(r <- rs) F r - \sum_(r <- rs | ~~ P r) F r.
+  Proof.
+    clear; intros.
+    induction rs; first by rewrite !big_nil subn0.
+    rewrite !big_cons !IHrs; clear IHrs.
+    case (P a); simpl; last by rewrite subnDl.
+    rewrite addnBA; first by done.
+    rewrite big_mkcond leq_sum //.
+    intros t _.
+      by case (P t).
+  Qed.
   
   Lemma telescoping_sum :
     forall (T: Type) (F: T->nat) r (x0: T),