feat(tactic/positivity): Handle a ≠ 0 goals

[YaelDillies]

Add some light postprocessing for positivity to prove goals of the form 0 ≠ a and a ≠ 0 when it can derive 0 < a.

---

The motivation for this is that side goals of order lemmas are sometimes a ≠ 0 because they hold for both 0 < a and a < 0.

This is only a fraction of what can be done in this direction. If you're happy with this, I will then make positivity fully handle a ≠ 0 hypotheses (rather than a simple postprocessing) by changing strictness to

meta inductive strictness : Type
| positive : expr → strictness
| nonnegative : expr → strictness
| nonzero : expr → strictness

This still works on a design level because there's a unique meaningful way of combining any two ≤, <, ≠ results. In particular, there won't be any branching.

[YaelDillies]

Closing in favor of #16529.