Use of Axiom of Choice for creating an infinitely decreasing sequence Suppose I have a set with total order but no least element $S$.
I create an infinitely decreasing sequence $ \{ a_i : i \in \mathbb N \} $ in the following way.
Now I pick one element $ a_1 \in S$.
I pick $ a_n$ such that $ a_n < a_i$ for all $ i \in \{1,..., n-1\}.$
Is the above construction correct or do I have to use axiom of choice for this sequence? 
 A: You used the fact that indeed the set $S$ has a countable subset, which is unbounded from below.
Indeed the first model of ZF without the axiom of choice was one where the real numbers has a subset $D$ which is of course linearly ordered; this subset was unbounded but alas has no decreasing sequence.
In fact every function from $\mathbb N$ into $D$ has a finite range (either increasing, decreasing, or both).
Note that indeed you only need to have some choice, in particular you need enough to allow an inductive definition on linear orders. This would be the principle of dependent choice or at least its restriction to linear orders.

The answer, in a nutshell, is that you have to use some choice to create this sequence. Enough to allow the inductive definition work "enough" to create the infinite sequence.
The set $D$ which I have mentioned is a Dedekind-finite set of real numbers, its existence contradicts the axiom of choice (indeed, even the axiom of countable choice). However since the existence of such set is not provable from ZF alone (it requires a rather strong negation of the axiom of choice) it is impossible to describe the set without resorting to a full tutorial about forcing, symmetric extensions and the axiom of choice.

Your proof is using the axiom of choice. Since you do not specify which element you choose at each step but rather just "pick" one, you have implicitly used some axiom of choice. It isn't wrong, indeed as I remark above - you cannot avoid it (in the general case). I do think that it is important to know where and how it comes into play. 
