diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 3ce75726e4..d172940a62 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -10,6 +10,8 @@
   + lemma `lipschitz_set0`, `lipschitz_set1`
 - in `measure.v`:
   + lemma `measurable_fun_bigcup`
+- in `sequences.v`:
+  + lemma `eq_eseriesl`
 
 ### Changed
 
diff --git a/theories/sequences.v b/theories/sequences.v
index f7ee417cd8..ca523a67ca 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -1576,6 +1576,11 @@ Lemma eq_eseriesr (R : realFieldType) (f g : (\bar R)^nat) (P : pred nat) :
   \sum_(i <oo | P i) f i = \sum_(i <oo | P i) g i.
 Proof. by move=> efg; congr (lim _); apply/funext => n; exact: eq_bigr. Qed.
 
+Lemma eq_eseriesl (R : realFieldType) (P Q : pred nat) (f : (\bar R)^nat) :
+  P =1 Q -> \sum_(i <oo | P i) f i = \sum_(i <oo | Q i) f i.
+Proof. by move=> efg; congr (lim _); apply/funext => n; exact: eq_bigl. Qed.
+Arguments eq_eseriesl {R P} Q.
+
 Section ereal_series.
 Variables (R : realFieldType) (f : (\bar R)^nat).
 Implicit Types P : pred nat.