diff --git a/util/sum.v b/util/sum.v
index 7d3e54e530d78d1e752611fdf5363a4927c075cd..35a05be923ebff3aeeaf889b5ef11d68d2ad1687 100644
--- a/util/sum.v
+++ b/util/sum.v
@@ -204,11 +204,7 @@ Section SumsOverRanges.
   Lemma sum_of_ones:
     forall t Δ,
       \sum_(t <= x < t + Δ) 1 = Δ. 
-  Proof.
-    move=> t Δ.
-    rewrite big_const_nat iter_addn_0.
-    by lia.
-  Qed.
+  Proof. by move=> t Δ; rewrite big_const_nat iter_addn_0 mul1n addKn. Qed.
 
   (** Next, we show that a sum of natural numbers equals zero if and only 
       if all terms are zero. *)