mathlib

0bdd47fa - feat(data/list/basic): add lemmas about list.take list.drop (#9245)

feat(data/list/basic): add lemmas about list.take list.drop (#9245) I added these lemmas about list.take and list.drop, which are present in Coq for example. Note that they are not entirely equivalent to list.take_append and list.drop_append because they also handle the case when `n ≤ l₁.length`