Co-authored-by: Johan Commelin <johan@commelin.net>

Adds a new positivity extension to handle integer exponents of value 0.
Corresponds to [this piece of logic](https://github.com/leanprover-community/mathlib/blob/09258fb7f75d741b7eda9fa18d5c869e2135d9f1/src/tactic/positivity.lean#L582-L584) in mathlib3.

This lets us uncomment another test case.

Adds `positivity` extensions for inversion, absolute value, and natAbs.

Compare the the mathlib3 versions [here](https://github.com/leanprover-community/mathlib/blob/3813d4ea1c6a34dbb472de66e73b8c6855b03964/src/tactic/positivity.lean#L535-L546), [here](https://github.com/leanprover-community/mathlib/blob/3813d4ea1c6a34dbb472de66e73b8c6855b03964/src/tactic/positivity.lean#L616-L631), and [here](https://github.com/leanprover-community/mathlib/blob/09258fb7f75d741b7eda9fa18d5c869e2135d9f1/src/tactic/positivity.lean#L633-L650).

For the absolute value case, I got stuck trying to make it work in the fully `Qq`-ified style, so I fell back to the `AppBuilder` style that's closer to how mathlib3 does it.

Co-authored-by: zeramorphic <50671761+zeramorphic@users.noreply.github.com>

Re-submit pull#1307 as a branch of mathlib4

Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Possible since leanprover/lean4#1984.  Thank you, Lean devs!

Closes #1336

As [reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linarith.20failure/near/319509822).

This should fix the problems in [#1319](#1319)

* Fixes a bug where `tauto` could try to work on a recursive auxiliary `LocalDecl`, potentially causing an error about well-founded recursion.
* Updates Data/Set/Intervals/UnorderedInterval.lean to use tauto, as per TODOs. The `not_mem_intervalOC` theorem is where I noticed the bug.
* Adds a test case isolated from `not_mem_intervalOC`.