feat(tactic/positivity): Handle `a ≠ 0` assumptions (#16529)
Make `positivity` handle `a ≠ 0` assumptions. This involves
* adding a third constructor to `positivity.strictness`, that I've called `nonzero`. It is meant to hold proofs of `a ≠ 0`, not `0 ≠ a`
* modifying the existing extensions to handle that new case.
* changing `positivity.orelse'` to account for the fact that if we can prove `0 ≤ a` and `a ≠ 0` then we can prove `0 < a`.
* making `compare_hyp` handle `eq` and `ne` hypotheses.
## Other changes
* Introduce `tac1 ≤|≥ tac2` as notation for `positivity.orelse' tac1 tac2`. This has the same precedence as the `<|>` notation for `orelse`.
* Make `positivity` extensions fail with more informative error messages. This is useless when running `positivity` alone but:
* It clearly marks within the code what each failure means
* The errors can show up when calling an extension directly. Not sure why you would do that, but you could.
* Add a `has_to_format strictness` instance. This is mostly useful for debugging.
