Baby Rudin Archimedean Property It was established in Baby Rudin that
If x is a positive real and y is a real, then there exists a natural number n such that nx>y.
It is then widely referenced in subsequent theorems without further explanation. I would like to verify whether this is correct or not.
In proving the existence of decimals in positive real, it was said that
Let x be a positive real and n be the greatest integer such that n is less than or equal to x.
The statement is immediately followed by "The existence of such n depends on the Archimedean property", However, this is less than or equal to instead of the greater than, which means it is not a direct application. So I wonder, is the following proof right, or can it be simplified?

*

*Denote $A=\{n\in\mathbb{Z^+}:n\geq x\}$

*By the Archimedean property, there exists $n_0\in\mathbb{Z^+}$ such that $n_0>x$

*The set is not empty

*Now consider the set $B=\{n-x:n\in\mathbb{Z^+}\land n\leq n_0\land n-x\geq 0\}$

*We know $n_0$ is finite so the set has finite members. As a result, the infimum equals minimum

*$x\in[\inf B-1+x,\inf B+x]$

*$n_0=\inf B-1+x\leq x$
Here I show there is an integer. Am I correct? The problem is not about the proof. The matter is about the degree which was ignored by Rudin. The proof applies the concept of infimum and order set. Archimedean property is just part of it.
So, is there better proof that uses the archimedean property?

Since an answer is still missing, I will try to fill this up:
Proof:
Let $x \in \mathbf{R}^+$. By the Archimedean Property, there exists $n \in \mathbf{Z}^+$ big enough such that $n > x$. Define the nonempty (why?) set
$$
A := \{ m \in \mathbf{Z}: 0 \leq m \leq n \}.
$$
Note that $A$ is finite as $n$ is. Now consider the nonempty (why?) set
$$
B := \{ m \in \mathbf{Z}: 0 \leq m \leq x \}.
$$
Then $B \subseteq A$ since $n > x$, so $B$ is finite and bounded above. Thus we can take $n_0 = \sup(B) \equiv \max(B)$ as desired. We leave why $\sup(B) \equiv \max(B)$ to the exercise below.
Exercise:
For any finite set $A \subseteq F$ on an ordered field $F$ (with the least upper bound principle, if we wish), we have
$$
\sup(A) = \max(A).
$$
Note:
Taking supremum and the exercise is not necessary if one knows any finite set on a totally ordered field has a maximum and a minimum. See for example, here: A finite set always has a maximum and a minimum.
