diff --git a/analysis/definitions/finish_time.v b/analysis/definitions/finish_time.v
new file mode 100644
index 0000000000000000000000000000000000000000..4cf10e0da4739245ca8776816353ff815114c488
--- /dev/null
+++ b/analysis/definitions/finish_time.v
@@ -0,0 +1,83 @@
+Require Export prosa.behavior.service.
+
+(** * Finish Time of a Job *)
+
+(** In this file, we define a job's precise finish time.
+
+    Note that in general a job's finish time may not be defined: if a job never
+    finishes in a given schedule, it does not have a finish time. To get around
+    this, we define a job's finish time under the assumption that _some_ (not
+    necessarily tight) response-time bound [R] is known for the job.
+
+    Under this assumption, we can simply re-use ssreflect's existing [ex_minn]
+    search mechanism (for finding the minimum natural number satisfying a given
+    predicate given a witness that some natural number satisfies the predicate)
+    and benefit from the existing corresponding lemmas. This file briefly
+    illustrates how this can be done. *)
+
+Section JobFinishTime.
+
+  (** Consider any type of jobs with arrival times and costs ... *)
+  Context {Job : JobType} `{JobArrival Job} `{JobCost Job}.
+
+  (** ... and any schedule of such jobs. *)
+  Context {PState : ProcessorState Job}.
+  Variable sched : schedule PState.
+
+  (** Consider an arbitrary job [j]. *)
+  Variable j : Job.
+
+  (** In the following, we proceed under the assumption that [j] finishes
+      eventually (i.e., no later than [R] time units after its arrival, for any
+      finite [R]). *)
+  Variable R : nat.
+  Hypothesis H_response_time_bounded : job_response_time_bound sched j R.
+
+  (** For technical reasons, we restate the response-time assumption explicitly
+      as an existentially quantified variable. *)
+  #[local] Corollary job_finishes : exists t, completed_by sched j t.
+  Proof. by exists (job_arrival j + R); exact: H_response_time_bounded. Qed.
+
+  (** We are now ready for the main definition: job [j]'s finish time is the
+      earliest time [t] such that [completed_by sched j t] holds. This time can
+      be computed with ssreflect's [ex_minn] utility function, which is
+      convenient because then we can reuse the corresponding lemmas. *)
+  Definition finish_time : instant := ex_minn job_finishes.
+
+  (** In the following, we demonstrate the reuse of [ex_minn] properties by
+      establishing three natural properties of a job's finish time. *)
+
+  (** First, a job is indeed complete at its finish time. *)
+  Corollary finished_at_finish_time : completed_by sched j finish_time.
+  Proof.
+    rewrite /finish_time/ex_minn.
+    by case: find_ex_minn.
+  Qed.
+
+  (** Second, a job's finish time is the earliest time that it is complete. *)
+  Corollary earliest_finish_time :
+    forall t,
+      completed_by sched j t ->
+      finish_time <= t.
+  Proof.
+    move=> t COMP.
+    rewrite /finish_time/ex_minn.
+    by case: find_ex_minn.
+  Qed.
+
+  (** Third, Prosa's notion of [completes_at] is satisfied at the finish time. *)
+  Corollary completes_at_finish_time :
+    completes_at sched j finish_time.
+  Proof.
+    apply/andP; split; last exact: finished_at_finish_time.
+    apply/orP; case FIN: finish_time; [by right|left].
+    apply: contra_ltnN => [?|];
+      first by apply: earliest_finish_time.
+    by lia.
+  Qed.
+
+  (** Finally, we can define a job's precise response time as usual as the time
+      from its arrival until its finish time. *)
+  Definition response_time : duration := finish_time - job_arrival j.
+
+End JobFinishTime.
diff --git a/behavior/service.v b/behavior/service.v
index 507ecddc6d16f0a308f7454ff62777af8967255c..6b7dd9e0aa6b8b16c5e13f7a07b7419b81a66f5e 100644
--- a/behavior/service.v
+++ b/behavior/service.v
@@ -43,8 +43,9 @@ Section Service.
   Definition completed_by (j : Job) (t : instant) := service j t >= job_cost j.
 
   (** We say that job [j] completes at time [t] if it has completed by time [t] but
-      not by time [t - 1]. *)
-  Definition completes_at (j : Job) (t : instant) := ~~ completed_by j t.-1 && completed_by j t.
+      not by time [t - 1] (or if [t == 0]). *)
+  Definition completes_at (j : Job) (t : instant) :=
+    (~~ completed_by j t.-1 || (t == 0)) && completed_by j t.
 
   (** We say that a constant [R] is a response time bound of a job [j] if [j]
       has completed by [R] units after its arrival. *)