Library prosa.analysis.facts.busy_interval.quiet_time

In this module we collect some basic facts about quiet times.

Section Facts.

Consider any kind of jobs...
  Context {Job : JobType} `{JobArrival Job} `{JobCost Job}.
... and a JLFP policy defined on these jobs.
  Context `{JLFP_policy Job}.
Consider any processor state model.
  Context {PState : ProcessorState Job}.

Consider any schedule and arrival sequence.
  Variable sched : schedule PState.
  Variable arr_seq : arrival_sequence Job.

We prove that 0 is always a quiet time.