Add a ListUtil lemma

1 files changed, 8 insertions, 0 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 3006dd799..49535da38 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -1097,6 +1097,14 @@ Qed.
 
 Hint Rewrite @sum_firstn_succ using congruence : simpl_sum_firstn.
 
+Lemma sum_firstn_succ_cons : forall x xs i,
+  sum_firstn (x :: xs) (S i) = (x + sum_firstn xs i)%Z.
+Proof.
+  unfold sum_firstn; simpl; reflexivity.
+Qed.
+
+Hint Rewrite @sum_firstn_succ_cons : simpl_sum_firstn.
+
 Lemma sum_firstn_succ_default_rev : forall l i,
   sum_firstn l i = (sum_firstn l (S i) - nth_default 0 l i)%Z.
 Proof.