I am not sure to what extend an analysis via Weihrauch reducibility is of interest to you, but I'll put it forth anyway. The fact that we are finicky about how often a principle is used here might make it easier to translate constructions into a choice-less context than eg arguments in Ishihara/Diener-style constructive reverse mathematics.

In this context, I called $\mathrm{CPO}$ robust division in [1], as it essentially lets us divide by a real number, if it might be $0$. The principle was relevant in the context of analyzing the existence of Nash equilibria in finite two player games. More results are in [2].

Key takeaways: $\mathrm{LLPO}$ is Weihrauch reducible to $\mathrm{CPO}$, but $\mathrm{CPO}$ is not Weihrauch reducible to any finite number of $\mathrm{LLPO}$-applications. $\mathrm{CPO}$ is strictly below both $\mathrm{LPO}$ and $\mathrm{IVT}$ (called "convex choice" $\mathrm{XC}_{[0,1]}$ in much of the Weihrauch reducibility literature).

A Weihrauch equivalent formulation over binary sequences would be: $$\forall p \in \mathbf{2}^\omega \ \exists q \in 2^\omega \ \ (p \neq 0^\omega) \rightarrow \exists k \in \mathbb{N} \ p = 0^k1q$$

[1] A.Pauly: "How non-computable is finding Nash equilibria", JUCS 2010 (https://doi.org/10.3217/jucs-016-18-2686)

[2] T.Kihara & A.Pauly: "Dividing by Zero - How Bad Is It, Really?", MFCS 2016, (https://drops.dagstuhl.de/opus/volltexte/2016/6470/)

I am not sure to what extend an analysis via Weihrauch reducibility (see [1] for an introduction/survey) is of interest to you, but I'll put it forth anyway. The fact that we are finicky about how often a principle is used here might make it easier to translate constructions into a choice-less context than eg arguments in Ishihara/Diener-style constructive reverse mathematics.

In this context, I called $\mathrm{CPO}$ robust division in [2], as it essentially lets us divide by a real number, if it might be $0$. The principle was relevant in the context of analyzing the existence of Nash equilibria in finite two player games. More results are in [3].

Key takeaways: $\mathrm{LLPO}$ is Weihrauch reducible to $\mathrm{CPO}$, but $\mathrm{CPO}$ is not Weihrauch reducible to any finite number of $\mathrm{LLPO}$-applications. $\mathrm{CPO}$ is strictly below both $\mathrm{LPO}$ and $\mathrm{IVT}$ (called "convex choice" $\mathrm{XC}_{[0,1]}$ in much of the Weihrauch reducibility literature).

A Weihrauch equivalent formulation over binary sequences would be: $$\forall p \in \mathbf{2}^\omega \ \exists q \in 2^\omega \ \ (p \neq 0^\omega) \rightarrow \exists k \in \mathbb{N} \ p = 0^k1q$$

[1] V.Brattka, G.Gherardi & A.Pauly: Weihrauch Complexity in Computable Analysis (http://arxiv.org/abs/1707.03202)

[2] A.Pauly: "How non-computable is finding Nash equilibria", JUCS 2010 (https://doi.org/10.3217/jucs-016-18-2686)

[3] T.Kihara & A.Pauly: "Dividing by Zero - How Bad Is It, Really?", MFCS 2016, (https://drops.dagstuhl.de/opus/volltexte/2016/6470/)