From 3c4993d2ae2ada2ef1416e45ac5a011071f6b302 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 11 Jan 2021 17:43:01 +0100
Subject: [PATCH] prove take_0

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

diff --git a/theories/list.v b/theories/list.v
index d8faeaf0..7b91cdd8 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1067,6 +1067,8 @@ Lemma take_drop_middle l i x :
 Proof.
   revert i x. induction l; intros [|?] ??; simplify_eq/=; f_equal; auto.
 Qed.
+Lemma take_0 l : take 0 l = [].
+Proof. reflexivity. Qed.
 Lemma take_nil n : take n [] =@{list A} [].
 Proof. by destruct n. Qed.
 Lemma take_S_r l n x : l !! n = Some x → take (S n) l = take n l ++ [x].
-- 
GitLab