Generalize definitions and lemmas in `analysis/facts/edf.v`

always_higher_priority and early_hep_job_is_scheduled are general facts about priority policies on uniprocessors that depend on neither EDF nor the ideal uniprocessor assumption.