add some reusable filtering lemmas on workload_of_jobs and arrivals_between, and use them to streamline a central EDF proof
workload_of_jobs
arrivals_between
@kbedarka — please review
FYI: @sbozhko