From 1ab781af059165e14cc253353f2d34ec92ddbc58 Mon Sep 17 00:00:00 2001
From: Jan Menz <s9jamenz@stud.uni-saarland.de>
Date: Mon, 7 Jun 2021 11:23:44 +0200
Subject: [PATCH] included Robbert's suggestions

---
 theories/list_numbers.v | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index 28c37363..a3fce30e 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -200,13 +200,10 @@ Section sum_list.
   Proof.
     induction l; simpl; rewrite ?reverse_cons, ?sum_list_with_app; simpl; lia.
   Qed.
-  Lemma sum_list_with_in x (f: A -> nat) l: x ∈ l -> f x ≤ sum_list_with f l.  
+  Lemma sum_list_with_in x (f: A → nat) l: x ∈ l → f x ≤ sum_list_with f l.  
   Proof.
-    intros H. induction l.
-    - contradict H. apply not_elem_of_nil. 
-    - cbn. rewrite elem_of_cons in H. destruct H as [H | H].
-      + simplify_eq. lia.
-      + specialize (IHl H). lia.
+    intros H. induction H.
+    all: simpl; lia.
   Qed.
   Lemma join_reshape szs l :
     sum_list szs = length l → mjoin (reshape szs l) = l.
-- 
GitLab