A revised version of !36 (closed), rebased on top of current master and addressing the comments raised in the discussion of the first version.
NOTE: I have changed the definition of "completed jobs don't execute" to make it more uniform and to be able to prove that "only ready jobs execute" implies that "completed jobs don't execute".
I think the old definition is an artifact of history and does not generalize well. For instance, on non-uniform speed processors, what if a job receives more than remaining_cost units of service in the last time instant that it is scheduled? In such a case, service <= cost is not actually true. So let's not bake it into a fundamental part of the library.
The invariant service <= cost is true, however, if we know service_at <= 1 (i.e., a unit-speed model), and hence this is now proved as a lemma in facts/completion.v.