diff --git a/CHANGELOG.md b/CHANGELOG.md
index b728eee9548e24044261ceb012d1d6428279fbd9..ae9279fe47c0ac36421ef5fd8e81c714fa68cac3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,6 +3,8 @@ API-breaking change is listed.
 
 ## std++ master
 
+- Add `list.zip_with_take_both` and `list.zip_with_take_both'`
+- Specialize `list.zip_with_take_{l,r}`, add generalized lemmas `list.zip_with_take_{l,r}'`
 - Add `bool_to_Z` that converts true to 1 and false to 0. (by Michael Sammler)
 - Add lemmas for lookup on `mjoin` for lists. (by Michael Sammler)
 - Rename `Is_true_false` → `Is_true_false_2` and `eq_None_ne_Some` → `eq_None_ne_Some_1`.
diff --git a/theories/list.v b/theories/list.v
index 3e24e7031f8a8d42e9a2937cd6a9bc7aecca60af..a884e8d2d732090937ee93484dea44e8f6b55569 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -4491,12 +4491,28 @@ Section zip_with.
   Proof.
     revert n k. induction l; intros [] []; f_equal/=; auto using zip_with_nil_r.
   Qed.
-  Lemma zip_with_take_l n l k :
-    length k ≤ n → zip_with f (take n l) k = zip_with f l k.
+  Lemma zip_with_take_l' n l k :
+    length l `min` length k ≤ n → zip_with f (take n l) k = zip_with f l k.
   Proof. revert n k. induction l; intros [] [] ?; f_equal/=; auto with lia. Qed.
-  Lemma zip_with_take_r n l k :
-    length l ≤ n → zip_with f l (take n k) = zip_with f l k.
+  Lemma zip_with_take_l l k :
+    zip_with f (take (length k) l) k = zip_with f l k.
+  Proof. apply zip_with_take_l'; lia. Qed.
+  Lemma zip_with_take_r' n l k :
+    length l `min` length k ≤ n → zip_with f l (take n k) = zip_with f l k.
   Proof. revert n k. induction l; intros [] [] ?; f_equal/=; auto with lia. Qed.
+  Lemma zip_with_take_r l k :
+    zip_with f l (take (length l) k) = zip_with f l k.
+  Proof. apply zip_with_take_r'; lia. Qed.
+  Lemma zip_with_take_both' n1 n2 l k :
+    length l `min` length k ≤ n1 → length l `min` length k ≤ n2 →
+    zip_with f (take n1 l) (take n2 k) = zip_with f l k.
+  Proof.
+    intros.
+    rewrite zip_with_take_l'; [apply zip_with_take_r' | rewrite take_length]; lia.
+  Qed.
+  Lemma zip_with_take_both l k :
+    zip_with f (take (length k) l) (take (length l) k) = zip_with f l k.
+  Proof. apply zip_with_take_both'; lia. Qed.
   Lemma Forall_zip_with_fst (P : A → Prop) (Q : C → Prop) l k :
     Forall P l → Forall (λ y, ∀ x, P x → Q (f x y)) k →
     Forall Q (zip_with f l k).