I was going to say this. The proof, unfortunately, sidelines into some very deep mathematics that it didn’t need to. I imagine but don’t know for sure that Euclid stopped where you do.
I’m not sure when infinite descent would be considered to have been formally proven to a modern mathematician but I bet it wasn’t in Euclid’s time!
I think the idea is that any strictly decreasing sequence of positive integers starting at N is a subsequence of (N, N-1, N-2, ..., 1) which has N elements, so any such sequence must have a finite number of elements.
So if you manage to produce an infinite sequence of strictly decreasing positive integers starting at a particular positive integer, then you've reached a contradiction.
Yes, I understand it intuitively, as would I think most non-suspicious people. It sounds very reasonable! As does the axiom of choice. We could even “prove” it using high school induction methods.
In practice though, concepts with infinity are very tricky, and the Greeks definitely did not have a strong accurate theory of infinity, Aleph-zero even, much less (as is the point talking about the sqrt(2)), the reals.
In this case, I think embedded in a high school proof would be the assumption that for any integer you can list there are not an infinite number smaller than them. This is manifestly true about the integers, but it is not true for the rationals, despite the two sets having the same cardinality, and a solid proof would need to be able to distinguish the reasons why. It’s this part that I think would be beyond the Greeks.
I’m not sure when infinite descent would be considered to have been formally proven to a modern mathematician but I bet it wasn’t in Euclid’s time!