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`





leanprover-community/mathlib,leanprover-community/mathlib