Using Axiom of Choice To Find Decreasing Sequences in Linear Orders Suppose I have a set along with a relation which is a total order. The set has no minimum element. Now, I want to create an infinite decreasing sequence of elements in this set. For this I have to use axiom of choice. But I'm not able to figure from which family of sets should I pick the elements so that I can use AoC. 
 A: For each $x\in X$, let $L_x = \{y\in X \mid y\lt x\}$. Take the family $\{L_x\}_{x\in X}$. Let $f$ be an element of $\prod_{x\in X}L_x$. 
Now pick $x_1\in X$. Use the recursion theorem to define a function $g\colon\mathbb{N}\to X$ by letting $g(1) = x_1$, and letting $g(n+1) = f(g(n))\in L_{g(n)}$. The sequence you want is $x_i=g(i)$. 

In fact, you don't need all of AC to do the above, it suffices to use the Axiom of Dependent Choice which is implied by, but is not equivalent to, the full Axiom of Choice. Showing that you actually need ADC for the general result (as opposed to showing that it suffices to use it) requires arguments along the lines of Asaf's answer.
A: Consider all the ordinals which can be embedded into the order inversely, that is order type forming decreasing chains in the linear order.
Let $\alpha$ be the supremum of all ordinals. If $\alpha<\omega$ then there is a minimal element; if $\alpha>\omega$ then we can inversely-embed $\omega$ and have the chain.
If $\alpha=\omega$, then we can use Zorn's lemma as follows:
Take all the decreasing chains ordered by extension. Every chain is bounded since the union of such chain gives a decreasing sequence. Therefore there exists a maximal element. Since we know that a finite chain can be extended by another element (otherwise a minimal element exists) the maximal element has an infinite length.
As Arturo remarked this can be done with Axiom of Dependent Choice, which is a restricted version of Zorn's lemma for partial orders whose height is $\omega$.

To see that the axiom of choice is needed, take the Basic Cohen model, that is add a Dedekind-finite set of reals. This set is totally ordered, it is unbounded and it has no countable subset. In particular we cannot find a countable sequence in this totally ordered set.

The exact choice strength is actually the one suggested by Arturo in the comments as a fragment of the Principle of Dependent Choice.
Let $\operatorname{DC}_{\operatorname{lin}}$ be the assertion that every linear ordering in which every finite chain can be extended has an increasing $\omega$-sequence.
Clearly, $\operatorname{DC}\Rightarrow\operatorname{DC}_{\operatorname{lin}}$, as $\operatorname{DC}$ speaks on non-linear orders as well. 
First note that this is obvious that $\operatorname{DC}_{\operatorname{lin}}$ implies that an ordering which is not bounded from below has a decreasing $\omega$-sequence. Inverse the order, as every finite (increasing) sequence can be extended (otherwise we hit a maximum) we have an $\omega$-sequence; inverse the order again and there we have it.
On the other hand, if $\operatorname{DC}_{\operatorname{lin}}$ does not hold then there is a linear order such that every finite increasing sequence can be extended but there is no $\omega$-sequence. In particular the inverse of such order will be a linear ordering with no least element, that has no decreasing $\omega$-sequence.
Question I: Suppose ZF+Exist an amorphous set. Since amorphous sets cannot be linearly ordered they cannot be used as counterexamples of $\operatorname{DC}_{\operatorname{lin}}$. 
Can there be a model of ZF+Exists an amorphous set+$\operatorname{DC}_{\operatorname{lin}}$? Can we relax the requirement of amorphous to an infinite Dedekind-finite set?
Question II: Can we have a model of ZF+$\operatorname{DC}{\operatorname{lin}}$+$\lnot\operatorname{AC}\omega$? 
That is a model in which ZF holds, $\operatorname{DC}_{\operatorname{lin}}$ holds but there is a countable family of sets without a choice function.
A: If you want to apply the axiom of choice directly, pay careful attention to what you're choosing:


*

*First, you choose an element $x_0 \in X$

*Second, you chose an element $x_1 \in \{ a \in X \mid a < x_0 \}$


Pay close attention to the second point -- we aren't really choosing an element from a set! Instead, we are choosing from a set-valued function of $x_0$, and so $x_1$ really should be a function of $x_0$!
Now how to apply choice is clear.


*

*First, you choose $x_0 \in x$

*Second, you choose $f_1$ from the subset $S_1$ of functions $X \to X$ satisfying $f(a) < a$

*Third, you choose $f_2$ from the subset $S_2$ of functions $X \times S_1 \to X$ satisfying $g(a,f) < a$ and $g(a,f) < f(a)$

*...


But to make things easier on ourselves, I will simplify:


*

*First, you choose $x_0 \in X$

*Second, you choose $f_1 : X \to X$ satisfying $f(a) < a$

*Third, you choose $f_2 : X^2 \to X$ satisfying $f(a,b) < a$ and $f(a,b) < b$ 

*...


Now, each of our sets is completely determined. We can show they are non-empty (by invoking induction and choice), and so we can apply choice to the collection.
Finally, our sequence is:


*

*$x_0$

*$x_1 = f_1(x_0)$

*$x_2 = f_2(x_0, x_1)$

*...


EDIT: just to make it explicit, the simplified version defines the sets $S_n$ to be the set of functions $g : X^n \to X$ satisfying $g(\vec{x}) < x_i$ for all $1 \leq i \leq n$.
(Depending on your tastes, you may want to special case $S_0 = X$)
For a choice $g \in S_n$, the value $g(\vec{x})$ is meant to be interpreted as "the choice I would make at at time $n$ if I had previously made the choices $x_0, x_1, \ldots, x_{n-1}$ at times $0, 1, \ldots, n-1$".
Now apply the axiom of choice to get a family of choices $f_n \in S_n$. Under the intended interpretation, our chosen decreasing sequence is
$$x_n = f_n(x_0, x_1, \ldots, x_{n-1})$$
(If you're special casing $0$, then $x_0 = f_0$ instead)
Of course, while this approach is systematic, it did not lead to the simplest result. At some point we might have recognized that our choice at time $n$ could be made to depend only on the choice made at time $n-1$ rather than the entire family of choices made at times $0$ through $n-1$. And if we do that, we might have then realized a single choice would work for all positive times. This would result in Arturo's answer.
