From 9869a4f842adb9b1ca1bd68a51f63d1a2e703d7f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Glen=20M=C3=A9vel?= <glen.mevel@inria.fr>
Date: Tue, 23 Nov 2021 17:55:19 +0100
Subject: [PATCH] add lemma `zip_with_take_both`

---
 theories/list.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index 4ecaf58e..a8e6d822 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -4474,6 +4474,11 @@ Section zip_with.
   Lemma zip_with_take_r n l k :
     length l ≤ 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_both l k :
+    zip_with f (take (length k) l) (take (length l) k) = zip_with f l k.
+  Proof.
+    rewrite zip_with_take_l; [apply zip_with_take_r | rewrite take_length]; 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).
-- 
GitLab