As the post points out this involves some claims about infinite sets that are maybe not super obvious to laypeople (every infinite set of natural numbers has a

As the post points out this involves some claims about infinite sets that are maybe not super obvious to laypeople (every infinite set of natural numbers has a least element). But we can rephrase this to avoid mentioning sets: For any rational number p/q (with q > 0) there exists a smallest positive natural number k such that k * p/q is natural: Clearly q works, so we check the finitely many numbers 1, ..., q and pick the smallest. Suppose the square root of 2 is rational. Let k be this smallest number for \sqrt 2, and proceed with the rest of the proof to find 0 < k' < k that also works.