What you just described is a classic proof of Brouwer's fixed point theorem using Sperner's lemma. The proof you cited earlier does not generalize to it on its own, the Sperner's lemma is a crucial combinatorial ingredient. It's crucial, because it only works on spaces with the topology of the triangle; you cannot perform the same argument on, say, an annulus.
In the standard formulation, you apply the Sperner's lemma to find smaller and smaller triangles, and apply compactness, precisely as in the standard proof of intermediate value theorem.
The rest of your post, where you quote reverse mathematics stuff, is completely irrelevant to the point I was making. Nothing I said is about what theorems follows from what axioms, but rather whether nonstandard analysis is meaningfully different, clearer, or more useful language than standard one. It is not.
In the standard formulation, you apply the Sperner's lemma to find smaller and smaller triangles, and apply compactness, precisely as in the standard proof of intermediate value theorem.
The rest of your post, where you quote reverse mathematics stuff, is completely irrelevant to the point I was making. Nothing I said is about what theorems follows from what axioms, but rather whether nonstandard analysis is meaningfully different, clearer, or more useful language than standard one. It is not.