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

remove 'wf' alias for the standard 'well_founded'

See merge request !524

solve_proper: add support for subrelation

See merge request !495

with tests

and more comments

Add `MThrow` and replace `MGuard`

See merge request !522