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.

mentioned in merge request !156 (merged)

This has been done in this commit : !156 (9cc286c2)

Thanks for digging up the commit. As far as I can tell, the lemma is still specific to ideal uniprocessors, so this issue is only half-closed.

marked this issue as related to #76 (closed)

Further progress is currently blocked on the fact that respects_policy_at_preemption_point is specific to ideal uniprocessors (#76 (closed)).

@sbozhko @kbedarka — Is this ticket still relevant after the aRTA generalization?

mentioned in commit 48f9065a

mentioned in commit 3a4bad28

mentioned in commit 1b2552ce

closed with commit 1b2552ce