diff --git a/restructuring/analysis/basic_facts/service.v b/restructuring/analysis/basic_facts/service.v
index f43be0f48494a36186c20e67152a0d8f062f3002..3b0e03899235ff5680318d2a9c2eed9d9ed70ac0 100644
--- a/restructuring/analysis/basic_facts/service.v
+++ b/restructuring/analysis/basic_facts/service.v
@@ -164,8 +164,8 @@ Section UnitService.
   Proof.
     unfold service_during; intros t delta.
     apply leq_trans with (n := \sum_(t <= t0 < t + delta) 1);
-      last by simpl_sum_const; rewrite addKn leqnn.
-      by apply: leq_sum => t' _; apply: service_at_most_one.
+      last by rewrite sum_of_ones.
+    by apply: leq_sum => t' _; apply: service_at_most_one.
   Qed.
 
   Section ServiceIsAStepFunction.
diff --git a/util/sum.v b/util/sum.v
index 1c61c685a591e145c507b6d007c2a02ff34a1c91..6249bd02808aa53b241c04539703e91c284f1145 100644
--- a/util/sum.v
+++ b/util/sum.v
@@ -248,7 +248,7 @@ Section ExtraLemmas.
       \sum_(t <= x < t + Δ) 1 = Δ. 
   Proof.
     intros.
-    simpl_sum_const.
+    rewrite big_const_nat iter_addn_0 mul1n.
     rewrite addnC -addnBA; last by done.
       by rewrite subnn addn0.  
   Qed.