minor

restructuring/analysis/fpp_implicit_deadline/intermediate.v

@@ -435,7 +435,8 @@ Proof.
     (n:=service sched j (end_of_analyse_interval)); auto.
   have /eqP<-: (t2 == end_of_analyse_interval); auto.
   have /eqP->: (len == t2 - t1); auto.
-  rewrite addnBCA. apply incr_service. apply leq_addr. 
+  rewrite addnBA. rewrite addnC -addnBA.
+  apply incr_service. apply leq_addr. 
   apply start_inf_arrival. rewrite ltnW; auto. apply start_inf_end.
 Qed.
 

restructuring/analysis/fpp_implicit_deadline/main_theorem.v

@@ -93,7 +93,8 @@ Section exists_t2.
   Let workload_bound := formula.
 
   Lemma exists_t2 : forall delta,
-    delta > 0 -> workload_bound delta = delta
+      delta > 0 -> workload_bound delta = delta
+      -> delta <= task_deadline tsk
       -> (forall j, arrives_in arr_seq j -> job_task j = tsk ->
     exists t2, job_arrival j < t2 /\ completes_at sched j t2).
   Proof.