diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index f6a7dd782ebccccdef7a1fb7f910fc1bb1af8f59..de29ac48c9541518ffa64796dfb951f87b1aa119 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -104,6 +104,16 @@ Section list.
   Lemma big_opL_unit l : ([^o list] k↦y ∈ l, monoid_unit) ≡ (monoid_unit : M).
   Proof. induction l; rewrite /= ?left_id //. Qed.
 
+  Lemma big_opL_take_drop Φ l n :
+    ([^o list] k ↦ x ∈ l, Φ k x) ≡
+    ([^o list] k ↦ x ∈ take n l, Φ k x) `o` ([^o list] k ↦ x ∈ drop n l, Φ (n + k) x).
+  Proof.
+    rewrite -{1}(take_drop n l) big_opL_app take_length.
+    destruct (decide (length l ≤ n)).
+    - rewrite drop_ge //=.
+    - rewrite Nat.min_l //=; lia.
+  Qed.
+
   Lemma big_opL_gen_proper_2 {B} (R : relation M) f (g : nat → B → M)
         l1 (l2 : list B) :
     R monoid_unit monoid_unit →
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 173ad7acdd08072d8fcd974201dacaa3539b6d96..1c901198a7189ccec62725de7577d9678fe529bc 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -98,6 +98,11 @@ Section sep_list.
     ([∗ list] k↦y ∈ l ++ [x], Φ k y) ⊣⊢ ([∗ list] k↦y ∈ l, Φ k y) ∗ Φ (length l) x.
   Proof. by rewrite big_opL_snoc. Qed.
 
+  Lemma big_sepL_take_drop Φ l n :
+    ([∗ list] k ↦ x ∈ l, Φ k x) ⊣⊢
+    ([∗ list] k ↦ x ∈ take n l, Φ k x) ∗ ([∗ list] k ↦ x ∈ drop n l, Φ (n + k) x).
+  Proof. by rewrite big_opL_take_drop. Qed.
+
   Lemma big_sepL_submseteq (Φ : A → PROP) `{!∀ x, Affine (Φ x)} l1 l2 :
     l1 ⊆+ l2 → ([∗ list] y ∈ l2, Φ y) ⊢ [∗ list] y ∈ l1, Φ y.
   Proof.