first use of `le_or_gt`

[mcol]

Lemma le_or_gt is used in example 2.5.2 without comment. Only further down in exercise 6, a short explanation is provided:

As in Example 2.5.2, I used the lemma le_or_gt, which says that if and are real numbers then either or ; it can be a useful case division

This should be moved to the place of first use.