Preemption model compliance

In this MR, we prove that the ideal uniprocessor schedules that are implemented in prosa.implementation.definitions.ideal_uni_scheduler respect the preemption model.

implementation/facts/ideal_uni/preemption_aware.v

@@ -150,8 +150,7 @@ Section NPUniprocessorScheduler.
             move: (H_chooses_from_set _ _ _ IN).
             rewrite mem_filter /backlogged => /andP [/andP [READY _]  _].
             rewrite -(H_nonclairvoyant_job_readiness (schedule_up_to policy idle_state t') schedule j t'.+1) //.
-            rewrite /identical_prefix /schedule /np_uni_schedule /generic_schedule => t'' LT.
-            now rewrite (schedule_up_to_prefix_inclusion _  _  t'' t') //. }
+            by apply schedule_up_to_identical_prefix. }
           case: (schedule_up_to _ _ t' t') => [j' | IN]; last by apply JOB.
           destruct (~~ job_preemptable j' _) eqn:NP => [EQ|IN]; last by apply JOB.
           apply H_valid_preemption_behavior.