to squash: one more corollary

analysis/definitions/finish_time.v

@@ -65,6 +65,19 @@ 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. *)
+  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: contra_ltnN => [?|];
+      first by apply: earliest_finish_time.
+    by lia.
+  Qed.
+
   (** Finally, we can define a job's precise response time as usual as the time
       from its arrival until its finish time. *)
   Definition response_time : duration := finish_time - job_arrival j.