Example of `have` expressions for proving termination

Stream: lean4

[ohhaimark]

When termination checking fails, it suggests

- Use `have`-expressions to prove the remaining goals

I couldn't find an example of this anywhere. How to I go about this?

[Henrik Böving]

https://leanprover.github.io/theorem_proving_in_lean4/induction_and_recursion.html?highlight=termination#well-founded-recursion-and-induction