fix `t = 0` cornercase in definition of `completes_at`

This definition isn't actually used anywhere important, maybe it's
time to get rid of it.

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