refactor(tactic/linarith): big refactor and docs (#3113)
This PR:
* Splits `linarith` into multiple files for organizational purposes
* Uses the general `zify` and `cancel_denom` tactics instead of weaker custom versions
* Refactors many components of `linarith`, in particular,
* Modularizes `linarith` preprocessing, so that users can insert custom steps
* Implements `nlinarith` preprocessing as such a custom step, so it happens at the correct point of the preprocessing stage
* Better encapsulates the FM elimination module, to make it easier to plug in alternate oracles if/when they exist
* Docs, docs, docs
The change to zification means that some goals which involved multiplication of natural numbers will no longer be solved. However, others are now in scope. `nlinarith` is a possible drop-in replacement; otherwise, generalize the product of naturals to a single natural, and `linarith` should still succeed.
Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
