`WellFoundedRelation` 型クラスを紹介する

これは decreasing_by を使用したときに参照される

cf. https://lean-lang.org/blog/2024-1-11-recursive-definitions-in-lean/

Often, the expression after termination_by is of type Nat. Then it is called a measure on the function arguments, and gives an upper bound on how often the function will make recursive calls. Generally, that expression can have any type α with a WellFoundedRelation α instance. This type class declares what it means for a value of α to be “smaller” to another (like < on Nat) and provides a proof that that relation is well-founded, meaning that starting from any value you can go to “smaller” values only a finite number of times.

Start with the linked Lean blog post and the WellFoundedRelation reference at Init/WF.html. Explain how WellFoundedRelation relates to termination_by and decreasing_by, using the scope described in the issue. Done means the documentation clearly introduces the type class and its well-founded ordering.