From Cut The Knot:
Let $P$ be a property that integers may or may not possess. If an assumption that a positive integer $n_0$ has property $P$ leads to the existence of a smaller positive integer $n_1<n_0$ that also satisfies $P$, then no positive integer has that property.
I intuitively get that we can show by contradiction that if $P$ holds for some natural number, then we get a sequence of infinite descent, which does not exist. But I’m not able to show the existence of such a sequence from assuming the contrary.
I also have a feeling that this would require AC since this (might?) involve choosing from a lot of possible sequences since there is no particular choice function I can think of from $P$.
I’d appreciate if you restrict only to natural numbers even though the above involves integers (so no subtraction is allowed).
One does not need AC to prove the existence of an infinite descending sequence, as there is a way to canonically choose the next element in the sequence. For example taking $n_{k+1}$ to be the greatest integer below $n_k$ satisfying $P$.
Technically, the function $f\colon n_k\mapsto n_{k+1}$ is definable in ZF, and then one can apply the recursion theorem (http://en.wikipedia.org/wiki/Recursion#The_recursion_theorem) to get that the sequence $(n_0,n_1,\dots)$ exists.