diff --git a/model/schedule/uni/schedule.v b/model/schedule/uni/schedule.v
index d0dd40c32c740bd8b64f405e933dbf150ca5bd80..afc93a02fd190fa4a1181a02871f5d75452e5853 100644
--- a/model/schedule/uni/schedule.v
+++ b/model/schedule/uni/schedule.v
@@ -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. *)