count): use + 1 instead of nat.succ (#17161)

Commit

3 years ago

chore(data/list/count): use + 1 instead of nat.succ (#17161) Also add `list.count_erase` and use `-1` instead of `nat.pred` in `list.count_erase_self`.

Author

urkud

Parents

f187f107

mathlib3 8b889832 - chore(data/list/count): use + 1 instead of nat.succ (#17161)

mathlib3
8b889832 - chore(data/list/count): use + 1 instead of nat.succ (#17161)