A tutorial on well-founded recursion in the Rocq proof assistant (previously known as Coq) https://gijs-pennings.github.io/rocq-wf-recursion