Added set lemmas about difference and union

See merge request !386

add map_fold_delete

See merge request !412

Add lemma `foldr_cons`.

See merge request !416

Add lemma `lookup_snoc_Some`.

See merge request !415

Add lemma `filter_app_complement`.

See merge request !414

add map_choose_or_empty

See merge request !413

Add bitvector library with automation

See merge request !408

Prepare changelog for release 1.8

See merge request !410

Refactor and improve documentation of feed and efeed tactics

See merge request !403

Refactor feed and add the feed generalize, efeed generalize, efeed inversion, and efeed destruct tactics

Rename plus/minus → add/sub and put number lemmas in modules to be consistent with Coq stdlib

See merge request !404

use the right list of authors..

Apply 2 suggestion(s) to 1 file(s)

remove highlights

This is similar to the trick we use for `bi` and makes it possible to import
`Nat` and obtain all lemmas---i.e., those from Coq's stdlib + those from std++.

Thanks to @Blaisorblade for the suggestion.

Rename `_plus`/`_minus` into `_add`/`_sub` to be consistent with Coq's current convention for numbers.

add some very basic f_equiv tests

See merge request !409