Refactor assumptions in a lemma about RBF
Lemma about task_rbf ε >= task_cost tsk
assumes that there exists a job of tsk
. However, the only goal of assuming the existence of a job is to obtain the fact that max_arrivals tsk ε > 0
. One can directly assume that the arrival curve is positive and hence remove the superfluous dependency.