do not rely on simpl_sum_const tactic

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.

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.