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. *)