From 2f13c73042a5e9c45353f7debda52cae4df72500 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre@roux01.fr>
Date: Sun, 20 Feb 2022 12:47:52 +0100
Subject: [PATCH] Simplify proof of sum_of_ones
---
util/sum.v | 6 +-----
1 file changed, 1 insertion(+), 5 deletions(-)
diff --git a/util/sum.v b/util/sum.v
index 7d3e54e53..35a05be92 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. *)
--
GitLab