Commit 726288f3 authored by sophie quinton's avatar sophie quinton

improve proof of completion_monotonic lemma

parent 9884f13e
......@@ -163,8 +163,7 @@ Module UniprocessorSchedule.
Proof.
unfold completed_by; move => t t' LE /eqP COMPt.
rewrite eqn_leq; apply/andP; split; first by apply H_completed_jobs.
by apply leq_trans with (n := service sched j t);
[by rewrite COMPt | by apply extend_sum].
rewrite- COMPt; by apply extend_sum.
Qed.
(* We also prove that a completed job cannot be scheduled. *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment