diff --git a/analysis/facts/transform/swaps.v b/analysis/facts/transform/swaps.v
index 70125852043c64e71e4e6b304be9f1933c1f11de..c8cd39e47526e4d3fdf0d56fcd436f3c116c2abc 100644
--- a/analysis/facts/transform/swaps.v
+++ b/analysis/facts/transform/swaps.v
@@ -248,10 +248,9 @@ Section SwappedFacts.
     rewrite /service !service_in_replaced// /service_at// /replace_at //.
     rewrite ifT// ifT// ifF;
       last by apply ltn_eqF; exact.
-    rewrite subn_abba //.
-    rewrite -(service_split_at_point _ _ _ t1 _) /service_at //.
-    apply leq_trans with (n := service_during sched j 0 t1 + service_in j (sched t1));
-      [rewrite addnC|]; by apply leq_addr.
+    have service_in_t1 : service_in j (sched t1) <= service_during sched j 0 t.
+    { by rewrite -(service_split_at_point _ _ _ t1 _)// addnAC leq_addl. }
+    by rewrite subnK ?(leq_trans service_in_t1) ?leq_addr// addnK.
   Qed.
 
   (** Finally, we note that, trivially, jobs that are not involved in
diff --git a/util/nat.v b/util/nat.v
index 0fd58b4b832153d0bac69628bc9a076c560a5a10..e14cf8acf9bb8872fe2493fc7edebbf2c91752b0 100644
--- a/util/nat.v
+++ b/util/nat.v
@@ -26,13 +26,6 @@ Section NatLemmas.
       m <= p - n.
   Proof. by intros; lia. Qed.
     
-  (** Simplify [n + a - b + b - a = n] if [n >= b]. *)
-  Lemma subn_abba:
-    forall n a b,
-      n >= b ->
-      n + a - b + b - a = 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,