More functions on lists.
Add the Coq repository:
opam repo add coq-released https://coq.inria.fr/opam/released
and run:
opam install coq-list-plus
Run:
./configure.sh
make
make install
Add:
Require Import ListPlus.All.
at the beginning of your source files.