fixup finish_time proof to match changed `completes_at` definition

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.