diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index 6e8a6ff06347b5d31f207191251242b637f7f586..7ca1548f4056d004ca305df0f85f8005e03a3ec5 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -200,6 +200,8 @@ 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) ls : x ∈ ls → f x ≤ sum_list_with f ls.
+  Proof. induction 1; simpl; lia. Qed.
   Lemma join_reshape szs l :
     sum_list szs = length l → mjoin (reshape szs l) = l.
   Proof.