diff --git a/theories/list.v b/theories/list.v
index d8faeaf085f458044b8cd1454d23d20c1cf7651c..7b91cdd80fa9b549bd9f709247a6cef2cbc570ea 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].