diff --git a/analysis/definitions/finish_time.v b/analysis/definitions/finish_time.v
index 18d92487dfe65f50c37ed54828d92a3e5252065f..4cf10e0da4739245ca8776816353ff815114c488 100644
--- a/analysis/definitions/finish_time.v
+++ b/analysis/definitions/finish_time.v
@@ -65,14 +65,12 @@ Section JobFinishTime.
     by case: find_ex_minn.
   Qed.
 
-  (** Third, when excluding the pathological case of a job completing at time
-      zero, Prosa's notion of [completes_at] is satisfied at the finish time. *)
+  (** Third, Prosa's notion of [completes_at] is satisfied at the finish time. *)
   Corollary completes_at_finish_time :
-    finish_time > 0 ->
     completes_at sched j finish_time.
   Proof.
-    move=> GT0.
     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.