Tiny improvements on the proof of the beta function lemma

[iblech]

The first commit very slightly sharpens the construction by making j a tiny bit smaller. (With the current definition of j, even the numbers x_0, ..., x_{n+1} will be relatively prime; a fact we don't need.)

The second commit adds an explicit witness to the relative primality of the x_i, obtained from the argument given in the text by proof mining. Personally, I'm interested in such things, but if you feel that the new footnote is a distraction, then please feel free to not merge the second commit.

I stumbled on the Open Logic Project only a couple of days ago. I'm amazed by its scope and quality. Thank you for your hard work in maintaining this project!

[rzach]

Thanks! I'm travelling right now and hope to review this in two weeks or so.

[iblech]

Just for the record, no hurry, I'm still on a page with my past self on this pull request :-), that is, I'm still in favor of these changes and could give additional justifications, if needed.