In this case you can define an order without using Choice. By definition of 'useful number' each useful number has some finite string that describes it. The finite strings can be put into lexicographic order, and then the useful numbers can be ordered according to the position of the lexicographically first string that describes them.
