Preemption model compliance

We show that the preemption-aware scheduler respects the preemption model semantics.

@bbb

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: