How can I use the principle of least integer to prove that a non-empty finite set of non-negative integers has a maximum element? Principle of least integer:  Every non-empty set of non-negative integers has a minimum element.
How can I use this principle to prove that a non-empty finite set of non-negative integers has a maximum element?
 A: I don't know if
least integer 
is the right method to use.
If I wanted to prove
the result,
I would try induction on
the number of elements in the set.
Since finite sets of integers
are defined by
starting with the empty set
and then inserting integers,
I would define max like this:
$\max(\emptyset) = 0$.
$\max(S \cup \{x\})
=\text{if } x > \max(S) \text{ then } x \text{ else } \max(S)
$.
My claim would be that,
if $\max$ is defined like this,
then
$\forall x \in S, \max(S) \ge x
$.
This would be proved by induction
on the size of $S$.
Note:
This discussion is 
highly influenced
by a class I took in
abstract data types
that was taught by
John Guttag
in the 1970's
at the USC
Computer Science department.
A: If $S$ is a finite set of nonnegative integers there is an $N\in{\mathbb N}$ such that $x< N$ for all $x\in S$. The set
$$S':=\{N-x\>|\>x\in S\}\subset{\mathbb N}$$
is nonempty, and therefore contains a smallest element $y_0$. The number $x_0:=N-y_0$ is then the maximal element of $S$.
A: Hint.  Let $\{x_1,\ldots,x_n\}$ be a non-empty finite set of non-negative integers.  Let $S$ be the sum $x_1+\cdots+x_n$, which is a (finite non-negative) integer.  Now consider
$$\{S-x_1,\,\ldots,\,S-x_n\}\ ,$$
which is a non-empty set of non-negative integers.
A: OK.
Here's a slightly weird way
of using the least integer principle
to find the maximum element.
It depends on having
a constructive form
of the principle
which returns the value
of the least element of
the set.
Let $LE(S)$ be a function
that returns the least element
of a nonempty set $S$ of
positive integers.
Then a function that returns
the maximum element of
a finite nonempty set
of positive integers
can be defined like this:
LEmax(S) = 
if |S|=1
then LE(S)
else LEmax(S \ LE(S)).
What this does
is check if the set has
only one element.
If so, that element
is the max
(and will be returned by
LE(S)).
If not,
get the least element,
remove it from the set,
and get the max of what remains.
To prove that this is correct
we can use the invariant
that if the set has
more than one element,
the max of the set is still there
because,
at each step,
an element less than the max
has been removed
(because the min and the max of the set are distinct).
Note:
Here is my definition of LE(S):
LE(S) =LE2(1, S)
LE2(n, S) =
if n $\in$ S then n
else LE2(n+1, S).
This starts at n=1 
and checks if n is in S.
If so, it returns n.
If not, it tries n+1.
A: Here's a proof sketch: Let $S$ denote a non-empty finite set of non-negative integers. Then by finiteness, $S$ has an upper bound. Write $U$ for the set of all upper bounds of $S$. We know that $U$ is inhabited. Hence by the principle of least integer (usually called the well-ordering principle), $U$ has a least element $u$. Now assume for a contradiction that $u$ is not the maximum element of $S$, and using the non-emptiness of $S$, try to derive a contradiction.
However: I prefer to conceptualize things a bit more. As I see it, what you really want to prove is: whenever $X$ is a non-empty totally-ordered set, if $X$ is finite, then $X$ has a maximum element. This is best viewed as a corollary of:

Theorem. Whenever $X$ is a partially-ordered set, if $X$ is finite, then every element of $X$ sits below some maximal element.

The proof uses the Axiom of dependent choice.
Proof sketch.
Let $X$ denote a partially-ordered set and $x$ denote an element thereof. Suppose toward a contradiction that $X_{\geq x}$ has no maximal element. Then it can be shown that $>$ is an entire relation on $X_{\geq x}$, by which I just mean that for all $y \in X_{\geq x}$, there exists $y' \in X_{\geq x}$ satisfying $y' > y$. Hence by dependent choice, there exists a function $f: X_{\geq x} \leftarrow \mathbb{N}$ satisfying: $$\mathop{\forall}_{n:\mathbb{N}}\;f(n+1)>f(n)$$
It can then be shown that $f$ is injective, and hence that $X_{\geq x}$ is infinite. But this implies that $X$ is infinite, a contradiction.
Further to that. If you want to learn more, I recommend reading up about well-foundedness. The story goes something like this:
Let $X$ denote a poset. Then assuming the axiom of choice, the following are equivalent (the first condition is easiest to visualize, and hence in some ways the most useful):


*

*Descending-chain condition. There is no $>$-preserving map $X \leftarrow \mathbb{N}$.

*Minimal-element condition. Every non-empty subset of $X$ has a minimal element.

*Transfinite induction. Suppose we're given a non-empty $A \subseteq X$ satisfying the following: for all $x \in X$, if $X_{<x} \subseteq A$, then $x \in A$. Then $A=X$.
We call posets $X$ satisfying one (and hence all three) of these conditions well-founded. For example, $\mathbb{N}$ is well-founded, but $\mathbb{Z}$ is not. Its important to understand that being finite implies being well-founded; in other words, well-foundedness generalizes finiteness. It can then be shown that every well-founded poset satisfies the "seat condition":


*

*Seat condition. Every element of $P$ sits above some minimal element.


The converse doesn't hold: for example, you can build a poset as follows. Start with an element $0$ and adjoin two elements below it. Forget about one of these, and focus on the other; now adjoin two elements below that. Forget about one of these, and focus on the other; now adjoin two elements below that. If you do this forever, you'll end up with an infinite tree that satisfies the seat condition, but which is not well-founded.
A: Let $S$ be a finite set of non-negative integers, and let $T$ be the set of non-negative integers that are larger than every element of $S$.
Because $S$ is finite, $T$ must be nonempty, therefore it has a minimum element $N$.
If $S$ is nonempty, then $N>0$, and $N-1$ is the maximum element of $S$.
A: If $X$ is your initial set, then take $A=\{n\in\mathbb{N}: n\geq x, \forall x \in X\}$. Prove $A$ is non-empty, then for PLI exits $n_0$ maximun element of $X$ 
