and the What4 symbolic simulator.

We use the EGCD algorithm to compute inverses for concrete values.
For symbolic values, we posit a multiplicitive inverse via a defining
equation.  To get this to work, we needed to fix a bug in the
equation definition code for What4; it was asserting definitions
with the wrong polarity for "prove" calls.

This involves adding the ability to assert definitional
relations, and porting the What4 method for modular inverse.

modular inverse computations instead of using the arithmoi and
semiring packages.

and finite field inverse computations.