This is another interesting example of induction which is often called relational induction. Here we define the less than or equal relation between natural numbers as the least fixed point of an operator. Now when we want to show that this is transitive, we just need to show that for a given new relation it is the case that this relation is a prefixed point for the operator defining the less than or equal relation. So at this point we know that the less than or equal relation is included in R, but by the way we have defined this relation we immediately have that the original relation is transitive. So as you see in fact these logical ways of reasoning on least fixed points and greatest fixed points do not really solve all the problems. We still have to apply some ingenuity in defining the inductive clauses. But once we have defined them then the machinery provides a way of reasoning rigorously. Other examples involve finite lists. We can see finite lists, least fixed points of this operator, finite trees of the other operator and so on.

---