Simplify edf2
- Some of the inequalities used in the EDF RTA to prove the soundness of IBF were not specific to EDF. These have been moved to
analysis.facts.busy_interval.inequalities
. - The lemma
reorder_summation
can be generalized to sums over partitions. Therefore, it has been moved toutil.sum
Edited by Kimaya Bedarkar