Modifications to ideal uniprocessor schedule

• We modified prev_job_nonpreemptive, as currently does respect jobs_must_be_ready_to_execute
• We do not prove schedule_respects_preemption_model anymore.
• We slightly changed valid_nonpreemptive_readiness so that sched is a parameter. This way, the proposition can be assumed to hold only for a certain schedule (making weaker assumptions).
• We proved more facts for the preemption-aware scheduler