Edf equivalence

Proving the equivalence of the predicates respects_policy_at_preemption_point and EDF_schedule - where both specify that a schedule is an EDF one (given an EDF priority definition).

analysis/facts/behavior/completion.v

@@ -33,6 +33,16 @@ Section CompletionFacts.
       by apply service_monotonic.
   Qed.
 
+  (** We prove that if j is not completed by t', then it's not completed by every instant before that. *)
+  Lemma incompletion_monotonic:
+    forall t t',
+      t <= t' ->
+      ~~ completed_by sched j t' ->
+      ~~ completed_by sched j t.
+  Proof.
+    move => t t' LE. apply contra. by apply completion_monotonic.
+  Qed.
+
   (** We observe that being incomplete is the same as not having received
      sufficient service yet... *)
   Lemma less_service_than_cost_is_incomplete: