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.