diff --git a/WorkloadDefsJitter.v b/WorkloadDefsJitter.v
index 2af331fc5274d307f9715ca8681fc668e555fd49..4ad4205ef894ad703854907c7cb1bdeeafc99946 100644
--- a/WorkloadDefsJitter.v
+++ b/WorkloadDefsJitter.v
@@ -541,7 +541,7 @@ Module WorkloadWithJitter.
           exploit (no_dl_misses j_fst INfst); last intros COMP.
           { 
             (* Prove that arr_fst + d_k <= t2 *)
-            apply leq_trans with (n := job_arrival j_lst); last by apply ltnW.
+            apply leq_ltn_trans with (n := job_arrival j_lst); last by done.
             apply leq_trans with (n := job_arrival j_fst + task_period tsk + delta); last by ins.
             rewrite -addnA leq_add2l -[job_deadline _]addn0.
             apply leq_add; last by ins.