diff --git a/behavior/service.v b/behavior/service.v
index 34e89f96a3970f1df8dcf38b0601661e1d6297b2..b4ff0fa7e745df08ed404dd3d26f19c2f6682005 100644
--- a/behavior/service.v
+++ b/behavior/service.v
@@ -17,6 +17,10 @@ Section Service.
 
   (** ... and the instantaneous service received by job j at time t. *)
   Definition service_at (j : Job) (t : instant) := service_in j (sched t).
+  
+  (** We say that a job [j] receives service at time [t] if
+      [service_at j t] is positive. *) 
+  Definition receives_service_at (j : Job) (t : instant) := 0 < service_at j t.
 
   (** Based on the notion of instantaneous service, we define the cumulative
       service received by job j during any interval from [t1] until (but not