diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index 6e8a6ff06347b5d31f207191251242b637f7f586..c9a39d2da43cbe62bdcaa495261bee2a911178de 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -200,6 +200,14 @@ 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.  
+  Proof.
+    intros. 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.
+  Qed.
   Lemma join_reshape szs l :
     sum_list szs = length l → mjoin (reshape szs l) = l.
   Proof.