Prove, without any Choice principles or Excluded Middle, that if a pointwise differentiable function has derivative $0$ everywhere, then it is constant. The function in this case maps $\mathbb R$ to $\mathbb R$, where $\mathbb R$ denotes the Dedekind reals. Unique Choice is allowed.

The usual proof of this proposition is via the Mean Value Theorem or the Law of Bounded Change. However the former is non-constructive, and the truth of the latter (in the absence of Dependent Choice) is an open problem.

Similar questions about elementary analysis in weak foundations have been asked before on this site. For instance, see: Approximate intermediate value theorem in pure constructive mathematics