Fix slowdown in bv_saturate from https://github.com/coq/coq/pull/17984

See merge request !541

Allow pattern and type annotations in propset notation

See merge request !533

Add lemma `join_app`.

See merge request !540

Adapt to https://github.com/coq/coq/pull/18590

See merge request !537

drop support for Coq 8.16 and 8.17

See merge request !539

test on Coq 8.19

See merge request !538

Adapt to https://github.com/coq/coq/pull/18224

See merge request !536

Remove Import NPeano

See merge request !535

Make `inv` and `oinv` work with numbers

Closes #199

See merge request !534

Add `prod_swap` and some basic results for it.

See merge request !529

Missing `Params` instances for `prod_map` and `prod_zip`.

See merge request !528

add inv and oinv tactics that are basically a smarter and fixed inversion_clear

Closes #40

See merge request !525

Add lemmas for easy measure/size induction.

See merge request !519