Unfold definitions commonly used in well founded relation definitions.
This is primarily intended for internal use in `decreasing_tactic`

.

## Instances For

Extensible helper tactic for `decreasing_tactic`

. This handles the "base case"
reasoning after applying lexicographic order lemmas.
It can be extended by adding more macro definitions, e.g.

```
macro_rules | `(tactic| decreasing_trivial) => `(tactic| linarith)
```

## Instances For

Constructs a proof of decreasing along a well founded relation, by applying
lexicographic order lemmas and using `ts`

to solve the base case. If it fails,
it prints a message to help the user diagnose an ill-founded recursive definition.

## Instances For

`decreasing_tactic`

is called by default on well-founded recursions in order
to synthesize a proof that recursive calls decrease along the selected
well founded relation. It can be locally overridden by using `decreasing_by tac`

on the recursive definition, and it can also be globally extended by adding
more definitions for `decreasing_tactic`

(or `decreasing_trivial`

,
which this tactic calls).