diff --git a/theories/list.v b/theories/list.v
index df5938b87d6865f28c4bebc0c8f731d3e4111d1e..d7ead7776c7b82da959d2f206939507ca1ca5e34 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -752,6 +752,14 @@ Proof.
   intros l1 l2 Hl.
   by rewrite <-(reverse_involutive l1), <-(reverse_involutive l2), Hl.
 Qed.
+Lemma sum_list_with_app (f : A → nat) l k :
+  sum_list_with f (l ++ k) = sum_list_with f l + sum_list_with f k.
+Proof. induction l; simpl; lia. Qed.
+Lemma sum_list_with_reverse (f : A → nat) l :
+  sum_list_with f (reverse l) = sum_list_with f l.
+Proof.
+  induction l; simpl; rewrite ?reverse_cons, ?sum_list_with_app; simpl; lia.
+Qed.
 
 (** ** Properties of the [last] function *)
 Lemma last_snoc x l : last (l ++ [x]) = Some x.