This is not a Coq proof, but it's a proof sketch using the axiom of dependent choice and LEM to exhibit an equivalence. I believe this is the weakest choice principle you can get away with, but I cannot find a reference. It's too long for a comment unfortunately.

Let's define $\mathsf{idc}(A,R,a)$ to be the proposition which states that there is an infinite descending chain in $(A,R)$ starting with $a$: $$ \mathsf{idc}(A,R,a) = \exists f : \mathbb{N} \to A.\ f(0) = a \land (\forall n.\ f(n) \mathrel{R} f(n + 1)) $$

We will show that $\neg \mathsf{idc}(A,R,a) \iff \mathsf{Acc}(A,R,a)$. The $\Leftarrow$ direction follows by induction on $\mathsf{Acc}$ and requires no non-constructive principles. The inductive step can be summarized as "if $\mathsf{idc}(A,R,a)$ holds, there is some $b$ such that $a \mathrel{R} b$ and $\mathsf{idc}(A,R,b)$ holds."

For the other direction, let's use LEM and assume $\neg \mathsf{Acc}(A,R,a)$ to derive a contradiction. We will achieve this contradiction by constructing an infinite descending chain and this is where we will use the axiom of dependent choice.

To that end, consider the type $B(a) = \{x : A \mid a \mathrel{R^*} x \land \neg \mathsf{Acc}(A,R,x)\}$ and write $S$ for the restriction of $R$ to this type. Let's prove that $S$ is entire, that is if $b : B(a)$ then there exists some $c$ such that $b \mathrel{S} c$. I've deferred this lemma to the bottom of the answer, to not clutter up the proof. Since $(B(a),S)$ is entire and non-empty with $a : B$ by assumption, the axiom of dependent choice gives us an infinite descending chain within $B(a)$: $b_0 \mathrel{S} b_1 \mathrel{S} b_2 \mathrel{S} b_3 \dots$. By definition of $S$, this induces a chain $b_0 \mathrel{R} b_1 \mathrel{R} b_2 \dots$. Moreover, by definition of $B(a)$ we can extend this chain so that it starts with $a$. We now derive our contradiction from $\neg\mathsf{idc}(A,R,a)$.

Lemma. $(B(a),S)$ is entire.

Proof. Assume we are given $b : B(a)$. By assumption, $\neg \mathsf{Acc}(A,R,b)$. Unfolding this, we see that it's equivalent to the following: $$ \neg (\forall b. a \mathrel{R} b \to \mathsf{Acc}(A,R,b)) $$

By LEM again, we obtain $c : A$ such that $a \mathrel{R} c$ and $\neg \mathsf{Acc}(A,R,c)$. Therefore, $c : B(a)$ and $b \mathrel{S} c$ as required.

This is not a Coq proof, but it's a proof sketch using the axiom of dependent choice and LEM to exhibit an equivalence. I believe this is the weakest choice principle you can get away with, but I cannot find a reference. It's too long for a comment unfortunately.

Edit: it's no longer just a paper proof! @kyo dralliam has formalized the below argument in Coq and gone further to show that the choice additional axioms (dependent choice, LEM) are also necessary as well as sufficient.

Let's define $\mathsf{idc}(A,R,a)$ to be the proposition which states that there is an infinite descending chain in $(A,R)$ starting with $a$: $$ \mathsf{idc}(A,R,a) = \exists f : \mathbb{N} \to A.\ f(0) = a \land (\forall n.\ f(n) \mathrel{R} f(n + 1)) $$

We will show that $\neg \mathsf{idc}(A,R,a) \iff \mathsf{Acc}(A,R,a)$. The $\Leftarrow$ direction follows by induction on $\mathsf{Acc}$ and requires no non-constructive principles. The inductive step can be summarized as "if $\mathsf{idc}(A,R,a)$ holds, there is some $b$ such that $a \mathrel{R} b$ and $\mathsf{idc}(A,R,b)$ holds."

For the other direction, let's use LEM and assume $\neg \mathsf{Acc}(A,R,a)$ to derive a contradiction. We will achieve this contradiction by constructing an infinite descending chain and this is where we will use the axiom of dependent choice.

To that end, consider the type $B(a) = \{x : A \mid a \mathrel{R^*} x \land \neg \mathsf{Acc}(A,R,x)\}$ and write $S$ for the restriction of $R$ to this type. Let's prove that $S$ is entire, that is if $b : B(a)$ then there exists some $c$ such that $b \mathrel{S} c$. I've deferred this lemma to the bottom of the answer, to not clutter up the proof. Since $(B(a),S)$ is entire and non-empty with $a : B$ by assumption, the axiom of dependent choice gives us an infinite descending chain within $B(a)$: $b_0 \mathrel{S} b_1 \mathrel{S} b_2 \mathrel{S} b_3 \dots$. By definition of $S$, this induces a chain $b_0 \mathrel{R} b_1 \mathrel{R} b_2 \dots$. Moreover, by definition of $B(a)$ we can extend this chain so that it starts with $a$. We now derive our contradiction from $\neg\mathsf{idc}(A,R,a)$.

Lemma. $(B(a),S)$ is entire.

Proof. Assume we are given $b : B(a)$. By assumption, $\neg \mathsf{Acc}(A,R,b)$. Unfolding this, we see that it's equivalent to the following: $$ \neg (\forall b. a \mathrel{R} b \to \mathsf{Acc}(A,R,b)) $$

By LEM again, we obtain $c : A$ such that $a \mathrel{R} c$ and $\neg \mathsf{Acc}(A,R,c)$. Therefore, $c : B(a)$ and $b \mathrel{S} c$ as required.