Job completion should be monotonic
The notion "a job is complete" is currently defined as:
Definition completed (t: time) := service t = job_cost j.
While correct, this has the unfortunate side effect that a job that receives more service than required — a pathological situation that we need to reason about in some proofs to cover all corner cases — reverts to being incomplete, which is intuitively nonsensical and requires us to have boiler-plate "complete jobs don't execute" assumptions all over the place.
It would be more convenient, and arguably more intuitive, to say:
Definition completed (t: time) := service t >= job_cost j.
That is, job completion should be monotonic.