Prove existence of abstract busy interval

Proofs of existence for busy intervals are usually quite long. They also depend on specific scheduling policy and preemption model. This leads to some unnecessary duplication. This commit introduces a proof of existence for abstract busy interval. The idea is to instantiate this proof for specific policies removing the duplication.