Commit 2021-09-18 02:27 0bdd47fa

View on Github →

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

Estimated changes

Modified src/data/list/basic.lean

added theorem list.drop_append_eq_append_drop

modified theorem list.drop_append_of_le_length

added theorem list.take_append_eq_append_take

modified theorem list.take_append_of_le_length