Is it possible to prove that every complex number has a square root using analytic LLPO, but avoiding Weak Countable Choice or Excluded Middle? Unique Choice is allowed.

(Analytic LLPO is the statement that given any pair of real numbers $x$ and $y$, either $x \leq y$ or $x \geq y$. This statement is non-constructive, but still weaker than other statements like LPO or Excluded Middle.)

It is true in Johnstone's Topological Topos. This is because the Fundamental Theorem of Algebra is true for Cauchy Real numbers, and Cauchy reals are isomorphic to Dedekind reals in the Topological Topos. But this reasoning doesn't seem to work unless Cauchy is iso to Dedekind.

Is it possible to prove that every complex number has a square root using analytic LLPO, but avoiding Weak Countable Choice or Excluded Middle? Unique Choice is allowed.

(Analytic LLPO is the statement that given any pair of real numbers $x$ and $y$, either $x \leq y$ or $x \geq y$. This statement is non-constructive, but still weaker than other statements like LPO or Excluded Middle.)

It is true in Johnstone's Topological Topos. This is because the Fundamental Theorem of Algebra is true for Cauchy Real numbers, and Cauchy reals are isomorphic to Dedekind reals in the Topological Topos. But this reasoning doesn't seem to work unless Cauchy is iso to Dedekind.