Question about Farey-like sequence I want a sequence of all rational fractions x/y with values from 0 to 1 in sorted order, where gcd(x, y) = 1 and x * y ≤ R for some given R ≥ 1. I'm told I can do this by starting with the fractions 0/1 and 1/1, then picking any two consecutive a/b and a'/b' in the sequence and inserting (a + a') / (b + b') between them, as long as (a + a')(b + b') ≤ R. For example with R = 15 the sequence would be
0/1, 1/15, 1/14, 1/13, ..., 1/5, 1/4, 1/3, 2/5, 1/2, 3/5, 2/3, 3/4, 1/1

But I can't prove that every fraction x/y will eventually be inserted into the sequence. I can start with the sequence [0/1, 1/1], then repeatedly find the two existing sequence elements before and after x/y, and insert an element between them according to the rule that was given. This must end when either I insert x/y, or when the number to be inserted has numerator * denominator > R, but I cannot prove that the second case won't happen.
For example, if R ≥ 35 then 5/7 would be inserted: Starting with [0/1, 1/1], insert 1/2 between them, then 2/3 between 1/2 and 1/1, then 3/4 between 2/3 and 1/1, then 5/7 between 2/3 and 3/4. However, I cannot prove that an arbitrary x/y would be added to the sequence in this way.
Any help? I assume there is either a proof so simple that I just cannot see it, or it is something really deep.
PS. I can produce the sequence by just generating all the elements and then sorting them, but that would be very unsatisfactory.
 A: "I cannot prove that an arbitrary x/y would be added to the sequence in this way."
The Cut the Knot link below shows how every reduced fraction will appear in a tree generated by successive mediants.  The Stern-Brocot tree is such a tree, whilst Farey sequences are extracts of the Stern-Brocot tree up to a given denominator.
https://www.cut-the-knot.org/blue/Stern.shtml
So now you can be assured that for any given x/y, calculating successive mediants will produce x/y in our list.
Suppose a/b and c/d cross-multiply to |1| and the denominator of their mediant is higher than our denominator of interest - and therefore that mediant will not be required in our sequence - now, how do we know that there is not some other fraction with a smaller denominator, lying between a/b and c/d?  That is, how do we know that a/b and c/d are next-door neighbours in our sequence and there is not some other fraction that we have missed in between them?
The answer to that question is given in this stackexchange post:
How prove that $q \geq b+d$ for $ad-bc = 1$ and $\frac{a}{b} > \frac{p}{q} > \frac{c}{d}$?
Having said all that, I see that you're not interested in a maximum denominator but in a maximum product of numerator and denominator.  So this answer is not what you need, but it may go part of the way.
