Choosing an inductive principle
Often, when proving things about an inductively defined function, it is useful to use the same inductive principle for the proof as was used for the definition. For example, we argued that the function is well-defined because it's second argument is decreasing (that is, while defining , we could assume that was already defined, since . This is a form of strong induction argument on . Therefore, a good heuristic for proving things about is to do induction on the second argument. That is, to prove "for all , some fact involving ", it makes sense to define as "for all , the fact involving ", and then use strong induction to prove for all .
The reason for this is that in the inductive step, you are likely to plug in the definition, and you would then like to apply the inductive hypothesis to reason about the expression you derive. If the inductive principle used in your proof matches the inductive principle used in your definition, you will be able to do this.