Remove work conservation dependence from the priority inversion file

• Currently the file prosa.analysis.facts.busy_interval.pi makes the assumption that the schedule is work-conserving (in the classic sense)
• Results from this file are used to bound the service inversion. Therefore the service inversion file also relies on the classic work conservation hypothesis.
• In this MR, I try to remove the work conservation hypothesis from some of the results in the PI file.
• Eventually, this will help us to remove the reliance of service inversion on the work conservation hypothesis.
• Removing the work conservation hypothesis crucially requires strengthening two lemmas regarding preemption.