Avoid restating lemma about distance between jobs
This lemma and facts about ordered jobs can be moved to a specific file:
Lemma workload_bound_many_periods_in_between : job_arrival j_lst - job_arrival j_fst >= num_mid_jobs.+1 * (task_period tsk).
This lemma and facts about ordered jobs can be moved to a specific file:
Lemma workload_bound_many_periods_in_between : job_arrival j_lst - job_arrival j_fst >= num_mid_jobs.+1 * (task_period tsk).