diff --git a/analysis/definitions/finish_time.v b/analysis/definitions/finish_time.v
index 3026d525807ca14aa4c5324158e1a2c6e57921f9..18d92487dfe65f50c37ed54828d92a3e5252065f 100644
--- a/analysis/definitions/finish_time.v
+++ b/analysis/definitions/finish_time.v
@@ -45,7 +45,7 @@ Section JobFinishTime.
   Definition finish_time : instant := ex_minn job_finishes.
 
   (** In the following, we demonstrate the reuse of [ex_minn] properties by
-      establishing two natural properties of a job's finish time. *)
+      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.