diff --git a/_CoqProject b/_CoqProject
index 8802c17cba70c2385cc3d0400313c55be48533ec..1590805a86a0b8599bb5daac5a7a499045d1289e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -20,5 +20,6 @@ link/flow_cc_of_arrival_sequence.v
 link/arrival_curve_of_request_bound_function.v
 link/request_bound_function_of_arrival_curve.v
 link/fifo.v
+link/delay.v
 
 COQDOCFLAGS = "-g -interpolate -utf8 --external https://math-comp.github.io/htmldoc/ mathcomp -R . NCCoq"
diff --git a/link/clock.v b/link/clock.v
index f70626ea3b4e81de3d27e98bbf5c7dde0e631432..5de504d5e54d4f91dcd2313ccc04d4628c3701eb 100644
--- a/link/clock.v
+++ b/link/clock.v
@@ -207,8 +207,7 @@ Record ppuclock := {
 Arguments Build_ppuclock : clear implicits.
 
 Lemma ppuclock_ub (c : ppuclock) n :
-  (uclock_tick_time c n.+1)%:nngnum
-  <= (uclock_tick_time c n)%:nngnum + (ppuclock_max_intertick c)%:num.
+  (c n.+1)%:nngnum <= (c n)%:nngnum + (ppuclock_max_intertick c)%:num.
 Proof. by case: c. Qed.
 
 (** Periodic clocks are a particular case of pseudo periodic clocks *)
@@ -230,3 +229,46 @@ rewrite (addrC (c (t + d)%nat)%:nngnum) addrACA.
 rewrite -(addn1 d) natrD mulrDl mul1r addrC.
 by apply: ler_add; rewrite ?(addrC (- _)) ?IHd// ler_subl_addl ppuclock_ub.
 Qed.
+
+Lemma next_tick_geqS (c : ppuclock) (t t' : {nonneg R}) :
+  t%:nngnum + (ppuclock_max_intertick c)%:num <= t'%:nngnum ->
+  ((next_tick c t).+1 <= next_tick c t')%N.
+Proof.
+move=> tMlet'; rewrite ltnNge; apply/negP => ntlt.
+move: tMlet'; apply/negP; rewrite -ltNge.
+have [| t'gt0 | ->] := ltgtP t'%:nngnum 0.
+{ by rewrite nngnum_lt0. }
+2:{ by rewrite -[0]addr0; apply: ler_lt_add. }
+have ntt'gt0 : (0 < next_tick c t')%N by rewrite next_tick_gt0.
+apply: (le_lt_trans (uclock_next_tick_gt c t')).
+rewrite -(ltn_predK ntt'gt0).
+apply: (le_lt_trans (ppuclock_ub _ _)).
+rewrite ltr_add2r.
+apply: uclock_lt_next_tick.
+by rewrite (ltn_predK ntt'gt0).
+Qed.
+
+Lemma next_tick_incr_lb (c : ppuclock) (t d : {nonneg R}) :
+  floor (d%:nngnum / (ppuclock_max_intertick c)%:num)
+  <= (next_tick c (t%:nngnum + d%:nngnum)%:nng%R - next_tick c t)%nat  :> int.
+Proof.
+set M := ppuclock_max_intertick c.
+set ddM := floor _.
+have: M%:num * ddM%:~R <= d%:nngnum.
+{ by rewrite mulrC -ler_pdivl_mulr// -RfloorE Rfloor_le. }
+case ddME: ddM => [n|n] dgem; [|exact: (@le_trans _ _ 0%:Z)].
+rewrite lez_nat leq_subRL; [|by apply: next_tick_leq; rewrite ler_addl].
+elim: n {ddM ddME} d dgem => [d _|n IHn d dgem].
+{ by rewrite addn0 next_tick_leq// ler_addl. }
+have dgeM : M%:num <= d%:nngnum.
+{ by apply: le_trans dgem; rewrite -add1n PoszD intrD mulrDr mulr1 ler_addl. }
+set td := _%:nng.
+pose dmM := insubd 0%:nng (d%:nngnum - M%:num).
+have tdgeM : t%:nngnum + dmM%:nngnum + M%:num <= td%:nngnum.
+{ by rewrite insubdK; [rewrite addrA subrK|rewrite /in_mem /= subr_ge0]. }
+apply: leq_trans (next_tick_geqS tdgeM).
+rewrite -addn1 addnA addn1 ltnS; apply: IHn.
+rewrite insubdK; [|by rewrite /in_mem /= subr_ge0].
+rewrite ler_subr_addr; apply: le_trans dgem.
+by rewrite -addn1 PoszD intrD mulrDr mulr1.
+Qed.
diff --git a/link/delay.v b/link/delay.v
new file mode 100644
index 0000000000000000000000000000000000000000..05cd9c7409483ea21058d078bdfed229ee741f59
--- /dev/null
+++ b/link/delay.v
@@ -0,0 +1,365 @@
+(** Link the notion of delay to the notion of response time in Prosa.
+
+    The two are equal providing a FIFO hypothesis inside tasks. *)
+
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype order ssrnat ssrint.
+From mathcomp Require Import choice seq path bigop ssralg ssrnum rat.
+From mathcomp Require Import fintype finfun.
+From mathcomp.analysis Require Import reals ereal nngnum posnum boolp classical_sets.
+Require Import prosa.util.nat prosa.util.bigcat prosa.util.sum.
+Require Import prosa.model.task.concept prosa.behavior.arrival_sequence prosa.analysis.definitions.schedulability.
+Require Import prosa.analysis.definitions.completion_sequence.
+Require Import nngenum RminStruct cumulative_curves deviations.
+Require Import clock flow_cc_of_arrival_sequence link.fifo.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
+
+Import Order.Theory GRing.Theory Num.Theory.
+
+Section Delay.
+
+Context {Task : TaskType}.
+Context {Job : JobType}.
+Context `{JobTask Job Task}.
+Context `{JobArrival Job}.
+
+Context {PState : Type}.
+Context `{ProcessorState Job PState}.
+Context `{JobReady Job PState}.
+Variable sched : schedule PState.
+
+(* TODO: hypothèse peu courante ? *)
+Hypothesis H_job_cost_positive : forall j, job_cost_positive j.
+
+(** * First consider only a single job *)
+
+(* TODO : move to Prosa? *)
+Definition arrival_sequence_of_job (j : Job) : arrival_sequence Job :=
+  fun t => if t == job_arrival j then [:: j] else [::].
+
+Lemma arrival_sequence_of_job_consistent j :
+  consistent_arrival_times (arrival_sequence_of_job j).
+Proof.
+move=> j' t.
+rewrite /arrives_at /arrivals_at /arrival_sequence_of_job.
+by case: eqP => [->|//]; rewrite in_cons orbF => /eqP ->.
+Qed.
+
+Lemma hDev_of_job_response_time (c : ppuclock) (j : Job)
+      (valid_sched : valid_schedule sched (arrival_sequence_of_job j))
+      A D d :
+  related_job_flow_cc c j A ->
+  related_arrival_flow_cc
+    c (job_task j) (completion_sequence (arrival_sequence_of_job j) sched) D ->
+  job_response_time_bound sched j d ->
+  ((hDev A D)%:nngenum <= (d%:R * (ppuclock_max_intertick c)%:num)%:E)%E.
+Proof.
+have arrival_times_are_consistent := @arrival_sequence_of_job_consistent j.
+have jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+{ exact/valid_schedule_implies_jobs_must_arrive_to_execute/valid_sched. }
+move=> -> -> j_rt.
+set arr_seq := arrival_sequence_of_job j.
+apply: ub_ereal_sup => _ [t _ <-].
+rewrite sup_horizontal_deviations le_maxl lee_fin; apply/andP; split=> [//|].
+apply: ub_ereal_sup => _ [d0 /= d0_lt <-].
+rewrite lee_fin leNgt; apply/negP => d0_gt; apply: negP d0_lt; rewrite -leNgt.
+case: (leP t%:nngnum _) => [_|tgtaj].
+{ rewrite lee_fin -sumrMnr; apply: sumr_ge0 => j' _; exact: ler0n. }
+rewrite lee_fin ler_nat.
+have -> : job_cost j = (\sum_(j <- [:: j]) job_cost j)%N.
+{ by rewrite big_cons big_nil addn0. }
+apply: leq_sum_sub_uniq => // j'; rewrite in_cons orbF => /eqP-> {j'}.
+rewrite mem_filter eqxx/=.
+have j_arr_in : arrives_in arr_seq j.
+{ exists (job_arrival j).
+  rewrite /arrivals_at /arr_seq /arrival_sequence_of_job /= eqxx.
+  by rewrite in_cons eqxx. }
+set cj := foldr minn (job_arrival j + d)%N
+                 [seq t <- iota 0 (job_arrival j + d) | completed_by sched j t].
+have cj_le_jd : (cj <= job_arrival j + d)%N.
+{ rewrite /cj; elim: filter => [//|x s /=]; exact/leq_trans/geq_minr. }
+have cj_compl : completed_by sched j cj.
+{ rewrite /cj; elim: iota => [//|x s IHs /=].
+  by case: ifP => [/=|//]; case: leqP. }
+have cj_ge_j : (job_arrival j <= cj)%N.
+{ rewrite leqNgt; apply/negP => cj_lt_j.
+  have j_cost0 : (job_cost j = 0)%N.
+  { apply: (completed_on_arrival_implies_zero_cost
+              _ _ jobs_must_arrive_to_execute).
+    apply: completion_monotonic cj_compl; exact: ltnW. }
+  by move: (H_job_cost_positive j); rewrite /job_cost_positive j_cost0. }
+have cjp_ncompl : ~~ completed_by sched j cj.-1.
+{ apply/negP => cjp_compl.
+  have cj_gt0 : (0 < cj)%N.
+  { case: cj cj_compl {cjp_compl cj_le_jd cj_ge_j} => [|//].
+    move: (H_job_cost_positive j).
+    by rewrite /completed_by service0 /job_cost_positive; case: job_cost. }
+  move: (cj_gt0); rewrite -ltn_predL; apply/negP; rewrite -leqNgt.
+  rewrite [in X in (X <= _)%N]/cj.
+  have cjp_lt_jd : (cj.-1 < job_arrival j + d)%N.
+  { by rewrite (ltn_predK cj_gt0). }
+  rewrite -(subnKC (ltnW cjp_lt_jd)) iotaD filter_cat foldr_cat add0n.
+  set x := foldr minn (_ + _)%N _.
+  have x_le_cjp : (x <= cj.-1)%N.
+  { rewrite /x -[(_ - cj.-1)%N](@ltn_predK 0%N) ?subn_gt0//= cjp_compl.
+    exact: geq_minl. }
+  elim: filter => [//|? s /=]; exact/leq_trans/geq_minr. }
+apply: (mem_bigcat_nat _ _ _ _ _ cj) => /=.
+2:{ rewrite mem_filter /completes_at cjp_ncompl cj_compl /=.
+    exact: job_in_arrivals_between. }
+apply: (leq_ltn_trans cj_le_jd).
+have jd_lt_ntct : (job_arrival j + d < next_tick c t + d)%N.
+{ rewrite ltn_add2r.
+  have j_arr : j \in arrivals_between arr_seq 0%N (next_tick c t).
+  { rewrite /arrivals_between.
+   apply: (@mem_bigcat_nat _ _ _ _ _ (job_arrival j)) => /=.
+    { rewrite ltnNge; apply/negP => H'.
+      move: tgtaj; rewrite ltNge => /negP; apply.
+      exact/(le_trans (uclock_next_tick_gt c _))/uclock_le. }
+    rewrite /arrivals_at /arr_seq /arrival_sequence_of_job /= eqxx.
+  by rewrite in_cons eqxx. }
+  by move: (in_arrivals_implies_arrived_between
+              _ arrival_times_are_consistent _ _ _ j_arr) => /andP[]. }
+apply: (leq_trans jd_lt_ntct).
+rewrite -lez_nat PoszD -ler_subr_addl subzn.
+2:{ by rewrite next_tick_leq// ler_addl. }
+apply: le_trans (next_tick_incr_lb _ _ _).
+rewrite -(ler_int R) -RfloorE -Rfloor_natz; apply: le_Rfloor.
+by rewrite ler_pdivl_mulr// ltW.
+Qed.
+
+Lemma job_response_time_of_hDev (c : uclock) (j : Job)
+      (valid_sched : valid_schedule sched (arrival_sequence_of_job j))
+      A D d :
+  related_job_flow_cc c j A ->
+  related_arrival_flow_cc
+    c (job_task j) (completion_sequence (arrival_sequence_of_job j) sched) D ->
+  ((hDev A D)%:nngenum <= (d%:R * (uclock_min_intertick c)%:num)%:E)%E ->
+  job_response_time_bound sched j d.
+Proof.
+have arrival_times_are_consistent := @arrival_sequence_of_job_consistent j.
+move=> -> -> /(le_trans (ereal_sup_ub _)).
+set s := hDev_at _ _.
+set mi2 := ((uclock_min_intertick c)%:num / 2)%:pos.
+set mi4 := ((uclock_min_intertick c)%:num / 2 / 2)%:pos.
+set t := ((c (job_arrival j))%:nngnum + mi4%:num)%:nng.
+move=> /(_ (s t)%:nngenum%E (ex_intro2 _ _ _ I erefl)).
+rewrite {}/s sup_horizontal_deviations le_maxl => /andP[_ hDev_d].
+apply/negPn/negP => ncompl_j; apply: negP hDev_d; rewrite -ltNge.
+pose d0 := (d%:R * (uclock_min_intertick c)%:num
+            + (uclock_min_intertick c)%:num / 2 / 2)%:nng.
+apply: (@lt_le_trans _ _ d0%:nngnum%:E).
+{ by rewrite /d0 addEFin lte_addl// lte_fin. }
+apply: ereal_sup_ub; exists d0 => [/=|//].
+set t' := ((c (job_arrival j))%:nngnum + mi2%:num)%:nng.
+set t'' := _%:nng.
+have -> : t'' = (t'%:nngnum + d%:R * (uclock_min_intertick c)%:num)%:nng.
+{ by apply/val_inj; rewrite /= addrACA [RHS]addrAC -posnum.splitr. }
+rewrite ifF; [|by apply/negbTE; rewrite -ltNge ltr_addl].
+rewrite lte_fin ltr_nat -[X in (_ < X)%N]addn0 -add1n.
+apply: leq_add; [exact: H_job_cost_positive|].
+set compl := filter _ _.
+suff -> : compl = [::] by rewrite big_nil.
+have ncompl_j' : j \notin compl.
+{ apply/negP => compl_j; apply: negP ncompl_j; apply/negPn.
+  rewrite /job_response_time_bound.
+  move: compl_j; rewrite mem_filter => /andP[_ /mem_bigcat_nat_exists[tj [/=]]].
+  rewrite mem_filter => /andP[/andP[_ +] _] tj_lt.
+  apply: completion_monotonic.
+  rewrite -ltnS -addSn; apply: (leq_trans tj_lt).
+  have <- : next_tick c t' = (job_arrival j).+1.
+  { apply: next_tick_eq => [|n'].
+    { apply: le_trans (uclock_incr _ _).
+      by rewrite ler_add2l ler_pdivr_mulr//= mulrDr mulr1 ler_addl. }
+    rewrite ltnS => /(uclock_le c) cn'_le.
+    by apply: (le_lt_trans cn'_le); rewrite ltr_addl. }
+  rewrite -lez_nat PoszD -ler_subl_addl subzn.
+  2:{ by rewrite next_tick_leq// ler_addl. }
+  apply: (le_trans (next_tick_incr_ub _ _ _)).
+  rewrite /= mulrK; [|exact: unitf_gt0].
+  by rewrite -(ler_int R) -RceilE /Rceil ler_oppl -mulrNz Rfloor_natz. }
+apply: filter_in_pred0 => j'.
+move: ncompl_j'; rewrite mem_filter eqxx/=.
+case: (@eqP _ j j'); [by move=> <- /[swap] ->|].
+move=> jnj' _.
+move=> /mem_bigcat_nat_exists[tj' [+ _]].
+rewrite mem_filter => /andP[_ /mem_bigcat_nat_exists[t'j' []]].
+rewrite /arrivals_at/arrival_sequence_of_job/=.
+case: ifP => // _; rewrite in_cons orbF eq_sym => jj'.
+by exfalso; apply/jnj'/eqP.
+Qed.
+
+(** * Then an entire task *)
+
+Lemma hDev_of_task_response_time (tsk : Task) (c : ppuclock)
+      (arr_seq : arrival_sequence Job)
+      (valid_arr_seq : valid_arrival_sequence arr_seq)
+      (valid_sched : valid_schedule sched arr_seq)
+      A D d :
+  related_arrival_flow_cc c tsk arr_seq A ->
+  related_arrival_flow_cc c tsk (completion_sequence arr_seq sched) D ->
+  task_response_time_bound arr_seq sched tsk d ->
+  ((hDev A D)%:nngenum <= (d%:R * (ppuclock_max_intertick c)%:num)%:E)%E.
+Proof.
+have [arrival_times_are_consistent arr_seq_is_a_set] := valid_arr_seq.
+have jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+{ exact/valid_schedule_implies_jobs_must_arrive_to_execute/valid_sched. }
+move=> -> -> tsk_rt.
+apply: ub_ereal_sup => _ [t _ <-].
+rewrite sup_horizontal_deviations le_maxl lee_fin; apply/andP; split=> [//|].
+apply: ub_ereal_sup => _ [d0 /= d0_lt <-].
+rewrite lee_fin leNgt; apply/negP => d0_gt; apply: negP d0_lt; rewrite -leNgt.
+rewrite lee_fin ler_nat.
+apply: leq_sum_sub_uniq => [|j]; [exact/filter_uniq/arrivals_uniq|].
+rewrite !mem_filter => /andP[/[dup] /eqP j_tsk -> /= j_arr].
+have j_arr_in : arrives_in arr_seq j by exact/in_arrivals_implies_arrived/j_arr.
+have j_rt : job_response_time_bound sched j d by exact: tsk_rt.
+set cj := foldr minn (job_arrival j + d)%N
+                 [seq t <- iota 0 (job_arrival j + d) | completed_by sched j t].
+have cj_le_jd : (cj <= job_arrival j + d)%N.
+{ rewrite /cj; elim: filter => [//|x s /=]; exact/leq_trans/geq_minr. }
+have cj_compl : completed_by sched j cj.
+{ rewrite /cj; elim: iota => [//|x s IHs /=].
+  by case: ifP => [/=|//]; case: leqP. }
+have cj_ge_j : (job_arrival j <= cj)%N.
+{ rewrite leqNgt; apply/negP => cj_lt_j.
+  have j_cost0 : (job_cost j = 0)%N.
+  { apply: (completed_on_arrival_implies_zero_cost
+              _ _ jobs_must_arrive_to_execute).
+    apply: completion_monotonic cj_compl; exact: ltnW. }
+  by move: (H_job_cost_positive j); rewrite /job_cost_positive j_cost0. }
+have cjp_ncompl : ~~ completed_by sched j cj.-1.
+{ apply/negP => cjp_compl.
+  have cj_gt0 : (0 < cj)%N.
+  { case: cj cj_compl {cjp_compl cj_le_jd cj_ge_j} => [|//].
+    move: (H_job_cost_positive j).
+    by rewrite /completed_by service0 /job_cost_positive; case: job_cost. }
+  move: (cj_gt0); rewrite -ltn_predL; apply/negP; rewrite -leqNgt.
+  rewrite [in X in (X <= _)%N]/cj.
+  have cjp_lt_jd : (cj.-1 < job_arrival j + d)%N.
+  { by rewrite (ltn_predK cj_gt0). }
+  rewrite -(subnKC (ltnW cjp_lt_jd)) iotaD filter_cat foldr_cat add0n.
+  set x := foldr minn (_ + _)%N _.
+  have x_le_cjp : (x <= cj.-1)%N.
+  { rewrite /x -[(_ - cj.-1)%N](@ltn_predK 0%N) ?subn_gt0//= cjp_compl.
+    exact: geq_minl. }
+  elim: filter => [//|? s /=]; exact/leq_trans/geq_minr. }
+apply: (mem_bigcat_nat _ _ _ _ _ cj) => /=.
+2:{ rewrite mem_filter /completes_at cjp_ncompl cj_compl /=.
+  exact: job_in_arrivals_between. }
+apply: (leq_ltn_trans cj_le_jd).
+have jd_lt_ntct : (job_arrival j + d < next_tick c t + d)%N.
+{ rewrite ltn_add2r.
+  by move: (in_arrivals_implies_arrived_between
+              _ arrival_times_are_consistent _ _ _ j_arr) => /andP[]. }
+apply: (leq_trans jd_lt_ntct).
+rewrite -lez_nat PoszD -ler_subr_addl subzn.
+2:{ by rewrite next_tick_leq// ler_addl. }
+apply: le_trans (next_tick_incr_lb _ _ _).
+rewrite -(ler_int R) -RfloorE -Rfloor_natz; apply: le_Rfloor.
+by rewrite ler_pdivl_mulr// ltW.
+Qed.
+
+Lemma task_response_time_of_hDev (tsk : Task) (c : uclock)
+      (arr_seq : arrival_sequence Job)
+      (valid_arr_seq : valid_arrival_sequence arr_seq)
+      A D d :
+  related_arrival_flow_cc c tsk arr_seq A ->
+  related_arrival_flow_cc c tsk (completion_sequence arr_seq sched) D ->
+  (* we must assume FIFO inside the task (for network calculus
+     says nothing about individual jobs in sequences) *)
+  FIFO_arrival_sequence sched arr_seq tsk tsk ->
+  ((hDev A D)%:nngenum <= (d%:R * (uclock_min_intertick c)%:num)%:E)%E ->
+  task_response_time_bound arr_seq sched tsk d.
+Proof.
+have [arrival_times_are_consistent arr_seq_is_a_set] := valid_arr_seq.
+move=> -> -> FIFO_tsk hDev_d.
+move=> j j_arr j_tsk.
+move: hDev_d => /(le_trans (ereal_sup_ub _)).
+set s := hDev_at _ _.
+set mi2 := ((uclock_min_intertick c)%:num / 2)%:pos.
+set mi4 := ((uclock_min_intertick c)%:num / 2 / 2)%:pos.
+set t := ((c (job_arrival j))%:nngnum + mi4%:num)%:nng.
+move=> /(_ (s t)%:nngenum%E (ex_intro2 _ _ _ I erefl)).
+rewrite {}/s sup_horizontal_deviations le_maxl => /andP[_ hDev_d].
+apply/negPn/negP => ncompl_j; apply: negP hDev_d; rewrite -ltNge.
+pose d0 := (d%:R * (uclock_min_intertick c)%:num
+            + (uclock_min_intertick c)%:num / 2 / 2)%:nng.
+apply: (@lt_le_trans _ _ d0%:nngnum%:E).
+{ by rewrite /d0 addEFin lte_addl// lte_fin. }
+apply: ereal_sup_ub; exists d0 => [/=|//].
+set t' := ((c (job_arrival j))%:nngnum + mi2%:num)%:nng.
+set t'' := _%:nng.
+have -> : t'' = (t'%:nngnum + d%:R * (uclock_min_intertick c)%:num)%:nng.
+{ by apply/val_inj; rewrite /= addrACA [RHS]addrAC -posnum.splitr. }
+have -> : next_tick c t = (job_arrival j).+1.
+{ apply: next_tick_eq => [|n'].
+  { apply: le_trans (uclock_incr _ _).
+    rewrite ler_add2l ler_pdivr_mulr//= ler_pdivr_mulr//.
+    rewrite -mulrA mulrDl mul1r -addrA mulrDr mulr1 ler_addl; exact: mulr_ge0. }
+  rewrite ltnS => /(uclock_le c) cn'_le.
+  by apply: (le_lt_trans cn'_le); rewrite ltr_addl. }
+rewrite lte_fin ltr_nat.
+set compls := completion_sequence _ _.
+set compl := filter _ _.
+set arr := filter _ _.
+rewrite [X in (_ < X)%N](perm_big (j :: [seq j' <- arr | j' != j])).
+2:{ apply: uniq_perm => [| |j'].
+  { exact/filter_uniq/arrivals_uniq. }
+  { rewrite cons_uniq mem_filter eqxx/=.
+    exact/filter_uniq/filter_uniq/arrivals_uniq. }
+  rewrite in_cons mem_filter.
+  case: eqP => [->|//].
+  rewrite mem_filter j_tsk eqxx/=.
+  rewrite /arrivals_between big_nat_recr//= mem_cat.
+  have [tj tj_arr] := j_arr.
+  by rewrite (arrival_times_are_consistent _ _ tj_arr) tj_arr orbT. }
+rewrite big_cons /= -[X in (X < _)%N]addn0 -addnS addnC.
+apply: leq_add; [exact: H_job_cost_positive|].
+apply: leq_sum_sub_uniq.
+{ exact/filter_uniq/completions_uniq. }
+have ncompl_j' : j \notin compl.
+{ apply/negP => compl_j; apply: negP ncompl_j; apply/negPn.
+  rewrite /job_response_time_bound.
+  move: compl_j; rewrite mem_filter => /andP[_ /mem_bigcat_nat_exists[tj [/=]]].
+  rewrite mem_filter => /andP[/andP[_ +] _] tj_lt.
+  apply: completion_monotonic.
+  rewrite -ltnS -addSn; apply: (leq_trans tj_lt).
+  have <- : next_tick c t' = (job_arrival j).+1.
+  { apply: next_tick_eq => [|n'].
+    { apply: le_trans (uclock_incr _ _).
+      by rewrite ler_add2l ler_pdivr_mulr//= mulrDr mulr1 ler_addl. }
+    rewrite ltnS => /(uclock_le c) cn'_le.
+    by apply: (le_lt_trans cn'_le); rewrite ltr_addl. }
+  rewrite -lez_nat PoszD -ler_subl_addl subzn.
+  2:{ by rewrite next_tick_leq// ler_addl. }
+  apply: (le_trans (next_tick_incr_ub _ _ _)).
+  rewrite /= mulrK; [|exact: unitf_gt0].
+  by rewrite -(ler_int R) -RceilE /Rceil ler_oppl -mulrNz Rfloor_natz. }
+move=> j' j'compl; rewrite mem_filter; apply/andP; split.
+{ by apply/negP => /eqP j'j; move: ncompl_j'; apply/negP/negPn; rewrite -j'j. }
+move: j'compl; rewrite !mem_filter => /andP[/[dup]+ ->] => j'tsk; rewrite andTb.
+move=> /mem_bigcat_nat_exists[tj' [/[dup] j'_compl]].
+rewrite mem_filter => /andP[_ j'arr] /andP[_ tj'_lt].
+have [aj'_le | aj'_gt] := leqP (job_arrival j') (job_arrival j).
+{ apply: job_in_arrivals_between => //.
+  exact: in_arrivals_implies_arrived j'arr. }
+have [tj [tj_le_tj' atj]]: exists tj, (tj <= tj')%N /\ arrives_at compls j tj.
+{ apply: (FIFO_tsk j j' (job_arrival j) (job_arrival j')) => //.
+  { by rewrite j_tsk. }
+  { have [tj tj_arr] := j_arr.
+    by rewrite (arrival_times_are_consistent _ _ tj_arr). }
+  have [aj' aj'a] := in_arrivals_implies_arrived _ _ _ _ j'arr.
+  by rewrite (arrival_times_are_consistent _ _ aj'a). }
+exfalso; apply: negP ncompl_j'; apply/negPn.
+rewrite mem_filter j_tsk eqxx /=.
+apply: mem_bigcat_nat atj => /=.
+exact: (leq_ltn_trans tj_le_tj').
+Qed.
+
+End Delay.