Remove leq_addk

leq_trans and leq_addr seem to be enough.

model/readiness/jitter.v

@@ -43,7 +43,7 @@ Section ReadinessOfJitteryJobs.
     move: H2 => /andP [REL UNFINISHED].
     rewrite /pending. apply /andP. split => //.
     move: REL. rewrite /is_released /has_arrived.
-    by apply leq_addk.
+    by apply: leq_trans; rewrite leq_addr.
   Qed.
 
 End ReadinessOfJitteryJobs.

model/readiness/suspension.v

@@ -52,7 +52,7 @@ Section ReadinessOfSelfSuspendingJobs.
     move: H2 => /andP [PASSED UNFINISHED].
     rewrite /pending. apply /andP. split => //.
     move: PASSED. rewrite /suspension_has_passed /has_arrived => /andP [ARR _].
-    by move: ARR; apply leq_addk.
+    by apply: leq_trans ARR; rewrite leq_addr.
   Qed.
 
 End ReadinessOfSelfSuspendingJobs.

util/nat.v

@@ -26,13 +26,6 @@ Section NatLemmas.
       m <= p - n.
   Proof. by intros; lia. Qed.
     
-  (** We can drop additive terms on the lesser side of an inequality. *)
-  Lemma leq_addk:
-    forall m n k,
-      n + k <= m ->
-      n <= m.
-  Proof. by intros; lia. Qed.
-    
   (** For any numbers [a], [b], and [m], either there exists a number
       [n] such that [m = a + n * b] or [m <> a + n * b] for any [n]. *)
   Lemma exists_or_not_add_mul_cases: