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

@@ -86,7 +86,7 @@ Section NPUniprocessorScheduler.
         by apply schedule_up_to_prefix_inclusion. }
       { elim: t IDLE NONE => [IDLE _| t' _ _ ->]; last by rewrite schedule_up_to_empty.
         rewrite /schedule_up_to replace_at_def.
-        rewrite /allocation_at /prev_job_nonpreemptive IDLE H_non_idling //. }
+        by rewrite /allocation_at /prev_job_nonpreemptive IDLE H_non_idling. }
     Qed.
 
     (** From the preceding fact, we conclude that the generated schedule is